instance PiBase.instIndiscreteTopologyOfR1SpaceOfPreirreducibleSpace {X : Type u} [TopologicalSpace X] [R1Space X] [i : PreirreducibleSpace X] : IndiscreteTopology X

Theorem T262: P134 (R1Space) + P39 (PreirreducibleSpace) => P129 (IndiscreteTopology)

theorem PiBase.Formal.T262 : P134 ⊓ P39 ≤ P129