instance PiBase.instCosmicSpaceOfAlephZeroSpace {X : Type u} [TopologicalSpace X] [h : AlephZeroSpace X] : CosmicSpace X

Theorem T241: P179 (AlephZeroSpace) => P74 (CosmicSpace)

theorem PiBase.Formal.T241 : P179 ≤ P74