instance PiBase.instInjPathConnectedSpaceOfArcConnectedSpace {X : Type u} [TopologicalSpace X] [h : ArcConnectedSpace X] : InjPathConnectedSpace X

Theorem T703: P95 (ArcConnectedSpace) => P38 (InjPathConnectedSpace)

theorem PiBase.Formal.T703 : P95 ≤ P38