theorem PiBase.instTopologicalNManifoldOfLocallyNEuclideanSpaceOfT2SpaceOfSecondCountableTopology {X : Type u} [TopologicalSpace X] [LocallyNEuclideanSpace X] [T2Space X] [SecondCountableTopology X] : TopologicalNManifold X

Theorem T31: P123 (LocallyNEuclideanSpace) + P3 (T2Space) + P27 (SecondCountableTopology) => P124 (TopologicalNManifold)

theorem PiBase.Formal.T31 : P123 ⊓ P3 ⊓ P27 ≤ P124