theorem PiBase.instT2SpaceOfContinuumSpace {X : Type u} [TopologicalSpace X] [ContinuumSpace X] : T2Space X

Theorem T481: P188 (ContinuumSpace) => P3 (T2Space)

theorem PiBase.Formal.T481 : P188 ≤ P3