let T be non empty TopSpace; :: thesis: for a, b, c being Point of T st a,b are_connected & b,c are_connected holds
a,c are_connected
let a, b, c be Point of T; :: thesis: ( a,b are_connected & b,c are_connected implies a,c are_connected )
assume that
A1: a,b are_connected and
A2: b,c are_connected ; :: thesis: a,c are_connected
set P = the Path of a,b;
set R = the Path of b,c;
A3: ( the Path of a,b is continuous & the Path of a,b . 0 = a ) by A1, BORSUK_2:def 2;
take the Path of a,b + the Path of b,c ; :: according to BORSUK_2:def 1 :: thesis: ( the Path of a,b + the Path of b,c is continuous & ( the Path of a,b + the Path of b,c) . 0 = a & ( the Path of a,b + the Path of b,c) . 1 = c )
A4: ( the Path of b,c . 0 = b & the Path of b,c . 1 = c ) by A2, BORSUK_2:def 2;
( the Path of a,b . 1 = b & the Path of b,c is continuous ) by A1, A2, BORSUK_2:def 2;
hence ( the Path of a,b + the Path of b,c is continuous & ( the Path of a,b + the Path of b,c) . 0 = a & ( the Path of a,b + the Path of b,c) . 1 = c ) by A3, A4, BORSUK_2:14; :: thesis: verum