instance PiBase.instHasCountableNetworkOfCosmicSpace {X : Type u_1} [TopologicalSpace X] [HasCountableNetwork X] [T3Space X] : CosmicSpace X

theorem PiBase.Formal.T61 : P182 ⊓ P5 ≤ P74