theorem PiBase.instT35SpaceOfT4Space {X : Type u} [TopologicalSpace X] [T4Space X] : T35Space X

Theorem T113: P7 (T4Space) => P6 (T35Space)

theorem PiBase.Formal.T113 : P7 ≤ P6