instance PiBase.instMetacompactSpaceOfParacompactSpace {X : Type u} [TopologicalSpace X] [h : ParacompactSpace X] : MetacompactSpace X

Theorem T14: P30 (ParacompactSpace) => P31 (MetacompactSpace)

theorem PiBase.Formal.T14 : P30 ≤ P31