theorem PiBase.instT1SpaceOfT6Space {X : Type u} [TopologicalSpace X] [T6Space X] : T1Space X

Theorem T152: P67 (T6Space) => P2 (T1Space)

theorem PiBase.Formal.T152 : P67 ≤ P2