theorem PiBase.instT3SpaceOfT35Space {X : Type u} [TopologicalSpace X] [T35Space X] : T3Space X

Theorem T115: P6 (T35Space) => P5 (T3Space)

theorem PiBase.Formal.T115 : P6 ≤ P5