proposition: Lemma subspace_open_char: forall U:Ensemble {x: X | In A x}, @open SubspaceTopology U <-> exists V:Ensemble X, open V /\ U = inverse_image subspace_inc V.
proof: Proof. apply weak_topology1_topology. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)