instance PiBase.instSymmetrizableSpaceOfSemimetrizableSpace {X : Type u} [TopologicalSpace X] [h : SemimetrizableSpace X] : SymmetrizableSpace X

Theorem T624: P102 (SemimetrizableSpace) => P104 (SymmetrizableSpace)

theorem PiBase.Formal.T624 : P102 ≤ P104