[STATEMENT]
lemma (in Order) mem_WWa_then:"W \<in> WWa D g a \<Longrightarrow> W \<subseteq> carrier D \<and> 
  Worder (Iod D W) \<and> a \<in> W \<and> (\<forall>x\<in>W. a \<preceq> x) \<and> 
  (\<forall>x\<in>W. (if (ExPre (Iod D W) x) then  g (Pre (Iod D W) x) = x else
  (if a \<noteq> x then Sup D (segment (Iod D W) x) = x else a = a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W \<in> WWa D g a \<Longrightarrow> W \<subseteq> carrier D \<and> Worder (Iod D W) \<and> a \<in> W \<and> (\<forall>x\<in>W. a \<preceq> x) \<and> (\<forall>x\<in>W. if ExPre (Iod D W) x then g (Pre (Iod D W) x) = x else if a \<noteq> x then Algebra2.Sup D (segment (Iod D W) x) = x else a = a)
[PROOF STEP]
by (simp add:WWa_def Wa_def)