instance PiBase.instkω3SpaceOfkω1SpaceOfK1T2Space {X : Type u} [TopologicalSpace X] [h : kω1Space X] [h' : K1T2Space X] : kω3Space X

Theorem T505: P98 (kω1Space) + P170 (K1T2Space) => P92 (kω3Space)

theorem PiBase.Formal.T505 : P98 ⊓ P170 ≤ P92