proposition: Lemma Exercise1_22c u: alls u (open_o r) -> open_o r (union u).
proof: Proof. move=> alo; split. by move=>t /setU_P [y ty yu]; move: (alo _ yu) => [p1 _]; apply: p1. move=> x y /setU_P [z xz zu] xy; move: (alo _ zu) => [_ p2]. apply /setU_P; exists z => //; exact (p2 _ _ xz xy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)