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