proposition: Lemma Exercise1_22y: lattice (reg_open_order r).
proof: Proof. move: (Exercise1_22x)=> [cl1 cl2]. by split => //u v => usr vsr; apply: cl2; move=> t; case/set2_P => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)