instance PiBase.instSubmetrizableSpaceOfHasCoarserSeparableMetrizableTopology {X : Type u} [TopologicalSpace X] [h : HasCoarserSeparableMetrizableTopology X] : SubmetrizableSpace X

Theorem T410: P166 (HasCoarserSeparableMetrizableTopology ) => P112 (SubmetrizableSpace)

theorem PiBase.Formal.T410 : P166 ≤ P112