let X be non empty TopSpace; for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
let a, b, c, d, e be Point of X; ( a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected implies for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic )
assume that
A1:
a,b are_connected
and
A2:
( b,c are_connected & c,d are_connected )
and
A3:
d,e are_connected
; for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
let A be Path of a,b; for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
let B be Path of b,c; for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
let C be Path of c,d; for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
let D be Path of d,e; ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
A4:
( A + (B + C),(A + B) + C are_homotopic & D,D are_homotopic )
by A1, A2, A3, BORSUK_2:12, BORSUK_6:73;
A5:
b,d are_connected
by A2, BORSUK_6:42;
then
a,d are_connected
by A1, BORSUK_6:42;
then A6:
(A + (B + C)) + D,((A + B) + C) + D are_homotopic
by A3, A4, BORSUK_6:75;
(A + (B + C)) + D,A + ((B + C) + D) are_homotopic
by A1, A3, A5, BORSUK_6:73;
hence
((A + B) + C) + D,A + ((B + C) + D) are_homotopic
by A6, BORSUK_6:79; verum