instance PiBase.instHasOpenPathComponentsOfWeaklyLocallySimplyConnectedSpace {X : Type u} [TopologicalSpace X] [h : WeaklyLocallySimplyConnectedSpace X] : HasOpenPathComponents X

Theorem T859: P231 (WeaklyLocallySimplyConnectedSpace) => P233 (HasOpenPathComponents)

theorem PiBase.Formal.T859 : P231 ≤ P233