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
consider P being Path of a,b, R being Path of b,c;
A3: ( P is continuous & P . 0 = a ) by A1, BORSUK_2:def 2;
take P + R ; :: according to BORSUK_2:def 1 :: thesis: ( P + R is continuous & (P + R) . 0 = a & (P + R) . 1 = c )
A4: ( R . 0 = b & R . 1 = c ) by A2, BORSUK_2:def 2;
( P . 1 = b & R is continuous ) by A1, A2, BORSUK_2:def 2;
hence ( P + R is continuous & (P + R) . 0 = a & (P + R) . 1 = c ) by A3, A4, BORSUK_2:17; :: thesis: verum