proposition: Lemma subspace_inc_continuous: @continuous SubspaceTopology X (@proj1_sig _ _).
proof: Proof. apply weak_topology1_makes_continuous_func. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)