fact: Definition second_countable (X:TopologicalSpace) : Prop := exists B : Family X, open_basis B /\ Countable B.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)