proposition: Lemma Exercise1_22v X: sub X (substrate (reg_open_order r)) -> least_upper_bound (reg_open_order r) X (open_bar r (union X)).
proof: Proof. move=> Xsr. have ou: (open_o r (union X)). apply: Exercise1_22c => // x xX; move: (Xsr _ xX) => /Exercise1_22s1P. by case. have oru: (open_r r (open_bar r (union X))) by apply: Exercise1_22i. have us: (inc (open_bar r (union X)) (substrate (reg_open_order r))). by apply /Exercise1_22s1P. have orr: (order (reg_open_order r)) by rewrite /reg_open_order; fprops. apply /(lubP orr Xsr);split. split => // y yX; move:(Xsr _ yX) => /Exercise1_22s1P oy. apply /Exercise1_22rP;split => //; apply: (@sub_trans (union X)). by apply: setU_s1. apply: Exercise1_22e => //. move=> z [] /Exercise1_22s1P oz h; apply /Exercise1_22rP;split => //. rewrite (Exercise1_22p oz); apply: Exercise1_22j =>//; first by case: oz. by move => w /setU_P [y wy yX]; move: (h _ yX) => /Exercise1_22rP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)