theorem PiBase.instDevelopableSpaceOfMooreSpace {X : Type u} [TopologicalSpace X] [MooreSpace X] : DevelopableSpace X

Theorem T715: P113 (MooreSpace) => P110 (DevelopableSpace)

theorem PiBase.Formal.T715 : P113 ≤ P110