theorem PiBase.instT2SpaceOfTopologicalNManifold {X : Type u} [TopologicalSpace X] [TopologicalNManifold X] : T2Space X

Theorem T333: P124 (TopologicalNManifold) => P3 (T2Space)

theorem PiBase.Formal.T333 : P124 ≤ P3