proposition: Lemma Exercise1_22w u v: open_r r u -> open_r r v -> sup (reg_open_order r) u v = open_bar r (u \cup v).
proof: Proof. move=> ou ov. have sd: (sub (doubleton u v) (substrate (reg_open_order r))). by move=> t; case/set2_P => ->; apply /Exercise1_22s1P. symmetry; apply: supremum_pr2; first by rewrite /reg_open_order; fprops. apply: (Exercise1_22v sd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)