instance PiBase.instT1SpaceOfSemiT2Space {X : Type u} [TopologicalSpace X] [h : SemiT2Space X] : T1Space X

Theorem T419: P169 (SemiT2Space) => P2 (T1Space)

theorem PiBase.Formal.T419 : P169 ≤ P2