theorem PiBase.instSecondCountableTopologyOfCountableOfFirstCountableTopology {X : Type u} [TopologicalSpace X] [Countable X] [FirstCountableTopology X] : SecondCountableTopology X

Theorem T212: P57 (Countable) + P28 (FirstCountableTopology) => P27 (SecondCountableTopology)

theorem PiBase.Formal.T212 : P57 ⊓ P28 ≤ P27