proposition: Lemma Exercise4_8d: let p:= fun U => [/\ sub U (irreds r), nonempty U & (forall x y, inc y U -> sup_irred r x -> gle r x y -> inc x U)] in (forall x, inc x (substrate r) -> p (E47S r x)) /\ (forall U, p U -> exists2 x, (inc x (substrate r)) & U = (E47S r x)).
proof: Proof. move: Exercise4_7b=> or p; split. move=> x xsr; split => //. by move=> t /Zo_P [pa [pb pc]]; apply /Zo_P. by apply: Exercise4_7h. move=> u v /Zo_P [vsr [su vx]] iu uv. apply /Zo_P; split => //; try split => //;order_tac. move=> U [p1 p2 p3]; rewrite (Exercise4_8c p1 p3 p2). exists (supremum r U) => //. have sU: sub U (substrate r). by move=> t tu; move: (p1 _ tu) => /Zo_P []. by move: (supremum_pr1 or (Exercise4_7i sU)) => /(lubP or sU) [[ok _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)