theorem PiBase.instSecondCountableTopologyOfFinite {X : Type u} [TopologicalSpace X] [Finite X] : SecondCountableTopology X

Theorem T189: P78 (Finite) => P27 (SecondCountableTopology)

theorem PiBase.Formal.T189 : P78 ≤ P27