instance PiBase.instRealcompactSpaceOfHereditarilyRealcompactSpace {X : Type u} [TopologicalSpace X] [h : HereditarilyRealcompactSpace X] : RealcompactSpace X

Theorem T740: P215 (HereditarilyRealcompactSpace) => P162 (RealcompactSpace)

theorem PiBase.Formal.T740 : P215 ≤ P162