theorem PiBase.instT3SpaceOfSigmaSpace {X : Type u} [TopologicalSpace X] [SigmaSpace X] : T3Space X

Theorem T84: P177 (SigmaSpace) => P5 (T3Space)

theorem PiBase.Formal.T84 : P177 ≤ P5