proposition: Lemma Exercise4_8c U: sub U (irreds r) -> (forall x y, inc y U -> sup_irred r x -> gle r x y -> inc x U) -> nonempty U -> U = (E47S r (supremum r U)).
proof: Proof. move: Exercise4_7b => or Usi hU neU. have sis: sub (irreds r) (substrate r) by apply: Zo_S. have Usr: sub U (substrate r) by apply: (@sub_trans (irreds r)). have fsU:= (sub_finite_set Usr fs). have hs := (lattice_finite_sup2 lr fsU neU Usr). move: (supremum_pr or Usr hs) => [[ub1 ub2] ub3]. set_extens t => ts. move: (ub2 _ ts) (Usi _ ts) => aux /Zo_P [p1 p2]. by apply /Zo_P;split => //; apply: Usr. move: ts => /Zo_P [tsr [srt ltsr]]. move: (Exercise4_8c1 tsr srt Usi ltsr neU) => [x sU tx]. exact: (hU _ _ sU srt tx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)