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

Theorem T716: P113 (MooreSpace) => P5 (T3Space)

theorem PiBase.Formal.T716 : P113 ≤ P5