instance PiBase.instMetrizableSpaceOfUltraMetrizableSpace {X : Type u} [τ : TopologicalSpace X] [h : UltraMetrizableSpace X] : TopologicalSpace.MetrizableSpace X

Theorem T770: P220 (UltraMetrizableSpace) => P53 (MetrizableSpace)

theorem PiBase.Formal.T770 : P220 ≤ P53