instance PiBase.instParacompactSpaceOfHereditarilyParacompact {X : Type u} [TopologicalSpace X] [h : HereditarilyParacompact X] : ParacompactSpace X

Theorem T744: P216 (HereditarilyParacompact) => P30 (ParacompactSpace)

theorem PiBase.Formal.T744 : P216 ≤ P30