theorem PiBase.instSecondCountableTopologyOfTopologicalNManifold {X : Type u} [TopologicalSpace X] [TopologicalNManifold X] : SecondCountableTopology X

Theorem T340: P124 (TopologicalNManifold) => P27 (SecondCountableTopology)

theorem PiBase.Formal.T340 : P124 ≤ P27