theorem PiBase.instFullyNormalSpaceOfFullyT4Space {X : Type u} [TopologicalSpace X] [FullyT4Space X] : FullyNormalSpace X

Theorem T337: P35 (FullyT4Space) => P34 (FullyNormalSpace)

theorem PiBase.Formal.T337 : P35 ≤ P34