let T be non empty TopSpace; :: thesis: ( T is trivial implies T is pathwise_connected )

assume A1: T is trivial ; :: thesis: T is pathwise_connected

let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected

take f = I[01] --> a; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )

thus f is continuous ; :: thesis: ( f . 0 = a & f . 1 = b )

a = b by A1;

hence ( f . 0 = a & f . 1 = b ) by BORSUK_1:def 14, BORSUK_1:def 15; :: thesis: verum

assume A1: T is trivial ; :: thesis: T is pathwise_connected

let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected

take f = I[01] --> a; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )

thus f is continuous ; :: thesis: ( f . 0 = a & f . 1 = b )

a = b by A1;

hence ( f . 0 = a & f . 1 = b ) by BORSUK_1:def 14, BORSUK_1:def 15; :: thesis: verum