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

Theorem T717: P110 (DevelopableSpace) + P5 (T3Space) => P113 (MooreSpace)

theorem PiBase.Formal.T717 : P110 ⊓ P5 ≤ P113