proposition: Lemma Exercise1_22b u: alls u (open_o r) -> open_o r (intersection u).
proof: Proof. move=> alo. have aux: forall t, inc t (intersection u) -> exists a, inc a u. move => t; case: (emptyset_dichot u). by move => ->; rewrite setI_0 => /in_set0. by move=> [a au] _; exists a. split. move=> t tu; move: (aux _ tu) => [a au]. move: (setI_hi tu au); move: (alo _ au) => [p1 _]; apply: p1. move=> x y xu xy; move: (aux _ xu) => [a au]. apply: setI_i; first by exists a;apply: au. move=> z zu; move: (alo _ zu) => [_ p2]; move: xy; apply: p2. exact (setI_hi xu zu). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)