instance PiBase.instSubmetrizableSpaceOfMetrizableSpace {X : Type u} [τ : TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] : SubmetrizableSpace X

Theorem T407: P53 (MetrizableSpace) => P112 (SubmetrizableSpace)

theorem PiBase.Formal.T407 : P53 ≤ P112