proposition: Lemma setU_sup1 s F E: sub F (\Po E) -> sub s F -> inc (union s) F -> least_upper_bound (sub_order F) s (union s).
proof: Proof. move=> Fp sF uF. have [oi si1] := (sub_osr F). have sss: sub s (substrate (sub_order F)) by ue. apply/(lubP oi sss); rewrite /upper_bound si1; split. by split => // y ys; apply /sub_gleP; split => //; fprops;apply: setU_s1. move=> z [zF hyp]; apply /sub_gleP; split => //. by apply: setU_s2=> y /hyp /sub_gleP [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)