proposition: Lemma Exercise1_22x: complete_lattice (reg_open_order r).
proof: Proof. have oro: (order (reg_open_order r)) by rewrite /reg_open_order; fprops. apply: Exercise1_11b => //. move=> X Xsr; exists (open_bar r (union X)); apply: (Exercise1_22v Xsr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)