instance PiBase.instPrepathConnectedSpaceOfUltraconnectedSpace {X : Type u} [TopologicalSpace X] [h : UltraconnectedSpace X] : PrepathConnectedSpace X

Theorem T38: P40 (UltraconnectedSpace) => P37 (PrepathConnectedSpace)

theorem PiBase.Formal.T38 : P40 ≤ P37