instance PiBase.instDiscreteTopologyOfHasOpenPathComponentsOfTotallyPathDisconnectedSpace {X : Type u} [TopologicalSpace X] [h : HasOpenPathComponents X] [h' : TotallyPathDisconnectedSpace X] : DiscreteTopology X

Theorem T89: P233 (HasOpenPathComponents) + P46 (TotallyPathDisconnectedSpace) => P52 (DiscreteTopology)

theorem PiBase.Formal.T89 : P233 ⊓ P46 ≤ P52