[STATEMENT]
lemma (in Worder) Tw_mem:"\<lbrakk>Worder E; x \<in> carrier D;
     \<forall>a\<in>carrier D. \<exists>b\<in>carrier E. ord_equiv (Iod D (segment D a))
         (Iod E (segment E b))\<rbrakk> \<Longrightarrow> (Tw\<^bsub>D,E\<^esub>) x \<in> carrier E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Worder E; x \<in> carrier D; \<forall>a\<in>carrier D. \<exists>b\<in>carrier E. ord_equiv (Iod D (segment D a)) (Iod E (segment E b))\<rbrakk> \<Longrightarrow> (Tw\<^bsub>D,E\<^esub>) x \<in> carrier E
[PROOF STEP]
by (frule Tw_func[of E], assumption,
       simp add:Pi_def)