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

Theorem T504: P92 (kω3Space) => P98 (kω1Space)

theorem PiBase.Formal.T504 : P92 ≤ P98