instance PiBase.instLocallyT2SpaceOfT2Space {X : Type u} [TopologicalSpace X] [T2Space X] : LocallyT2Space X

Theorem T193: P3 (T2Space) => P84 (LocallyT2Space)

theorem PiBase.Formal.T193 : P3 ≤ P84