proposition: Lemma Exercise1_22F E X: sub X E -> open_r (diagonal E) X.
proof: Proof. move=> XE. move: (diagonal_osr E) => [oi si]. have h: (forall x y, gle (diagonal E) x y -> x = y). by move=> x y /diagonal_pi_P [_]. split. split; [ue |by move=> x y xE xy; rewrite - (h _ _ xy) ]. move=> v [sv ov] cf; apply: extensionality => //. move: (proj1 cf); rewrite iorder_sr //. move=> t tv; move: cf => /(cofinal_inducedP oi sv) [_ cof]. by move: (cof _ tv)=> [y yX le]; rewrite (h _ _ le). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)