proposition: Lemma setI_inf1 s F E (T := (Yo (nonempty s) (intersection s) E)): sub F (\Po E) -> sub s F -> inc T F -> greatest_lower_bound (sub_order F) s T.
proof: Proof. rewrite /T;move=> Fp sF ssF. have [oi si1] := (sub_osr F). have sss: sub s (substrate (sub_order F)) by ue. apply/(glbP oi sss); rewrite /lower_bound si1; split. split =>// y ys; apply /sub_gleP; split; fprops. have nes: (nonempty s) by exists y. Ytac0;apply: setI_s1=>//. move=>z [zF hyp]; apply /sub_gleP; split => //. case: (emptyset_dichot s) => sp. by rewrite Y_false;[apply /setP_P /Fp | rewrite sp; move /nonemptyP ]. Ytac0;move=> t tz; apply: setI_i=>//. by move=> y /hyp /sub_gleP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)