instance PiBase.instLocallyInjPathConnectedSpaceOfLocallyArcConnectedSpace {X : Type u} [TopologicalSpace X] [h : LocallyArcConnectedSpace X] : LocallyInjPathConnectedSpace X

Theorem T704: P96 (LocallyArcConnectedSpace) => P43 (LocallyInjPathConnectedSpace)

theorem PiBase.Formal.T704 : P96 ≤ P43