instance PiBase.instLoallycPathConnectedSpaceOfAlexandrovDiscrete {X : Type u} [TopologicalSpace X] [h : AlexandrovDiscrete X] : LocallyPathConnectedSpace X

Theorem T316: P90 (AlexandrovDiscrete) => P42 (LocallyPathConnectedSpace)

theorem PiBase.Formal.T316 : P90 ≤ P42