let T be non empty TopSpace; 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; ( 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
; 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
; BORSUK_2:def 1 ( 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; verum