proposition: Lemma weak_topology1_makes_continuous_func: continuous f (X:=WeakTopology1).
proof: Proof. exact (weak_topology_makes_continuous_funcs _ _ _ (True_rect f) I). Qed.
imports: TopologicalSpaces Subbases Continuity Nets ZornsLemma(FiniteIntersections)