proposition: Lemma inf_inclusion A x y: sub x A -> sub y A -> greatest_lower_bound (subp_order A) (doubleton x y) (x \cap y).
proof: Proof. move=> xA yA. have sd: (sub (doubleton x y) (\Po A)) by apply: sub_set2; apply/setP_P. move: (setI_inf sd);rewrite Y_true //; apply: set2_ne. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)