instance PiBase.instDiscreteTopologyOfHasOpenConnectedComponentsOfTotallyDisconnectedSpace {X : Type u} [TopologicalSpace X] [h : HasOpenConnectedComponents X] [h' : TotallyDisconnectedSpace X] : DiscreteTopology X

Theorem T108: P234 (HasOpenConnectedComponents) + P47 (TotallyDisconnectedSpace) => P52 (DiscreteTopology)

theorem PiBase.Formal.T108 : P234 ⊓ P47 ≤ P52