theorem PiBase.instIsCompletelyMetrizableSpaceOfDiscreteTopology {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : TopologicalSpace.IsCompletelyMetrizableSpace X

Theorem T85: P52 (DiscreteTopology) => P55 (IsCompletelyMetrizableSpace)

theorem PiBase.Formal.T85 : P52 ≤ P55