theorem PiBase.instT1SpaceOfFullyT4Space {X : Type u} [TopologicalSpace X] [FullyT4Space X] : T1Space X

Theorem T104: P35 (FullyT4Space) => P2 (T1Space)

theorem PiBase.Formal.T104 : P35 ≤ P2