instance PiBase.instHasOpenPathComponentsOfPrepathConnectedSpace {X : Type u} [TopologicalSpace X] [h : PrepathConnectedSpace X] : HasOpenPathComponents X

Theorem T860: P37 (PrepathConnectedSpace) => P233 (HasOpenPathComponents)

theorem PiBase.Formal.T860 : P37 ≤ P233