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