proposition: Lemma setP_lattice_pr A x y (r := subp_order A): inc x (\Po A) -> inc y (\Po A) -> (sup r x y = x \cup y /\ inf r x y = x \cap y).
proof: Proof. move => /setP_P xA /setP_P yA. have or := (proj1 (setP_lattice A)). move: (inf_inclusion xA yA) (sup_inclusion xA yA) => pa pb. by rewrite (infimum_pr2 or pa) (supremum_pr2 or pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)