theorem PiBase.instT1SpaceOfT5Space {X : Type u} [TopologicalSpace X] [T5Space X] : T1Space X

Theorem T100: P8 (T5Space) => P2 (T1Space)

theorem PiBase.Formal.T100 : P8 ≤ P2