fact: Definition first_countable (X:TopologicalSpace) : Prop := forall x:point_set X, exists NBx:Family X, neighborhood_basis NBx x /\ Countable NBx.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)