instance PiBase.instStrnglyConnectedSpaceOfPseudocompactSpace {X : Type u_1} [TopologicalSpace X] [h : StronglyConnectedSpace X] : PseudocompactSpace X

theorem PiBase.Formal.T76 : P60 ≤ P22