proposition: Lemma second_countable_subbasis: forall (X:TopologicalSpace) (SB : Family X), subbasis SB -> Countable SB -> second_countable X.
proof: Proof. intros. eexists; split. { apply finite_intersections_of_subbasis_form_open_basis. eassumption. } apply finite_intersections_countable. assumption. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)