let X be non empty TopSpace; :: thesis: for a, b, c, d being Point of X st a,b are_connected & b,c are_connected & b,d are_connected holds
for A being Path of a,b
for B being Path of d,b
for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic
let a, b, c, d be Point of X; :: thesis: ( a,b are_connected & b,c are_connected & b,d are_connected implies for A being Path of a,b
for B being Path of d,b
for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic )
assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: b,d are_connected ; :: thesis: for A being Path of a,b
for B being Path of d,b
for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic
let A be Path of a,b; :: thesis: for B being Path of d,b
for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic
let B be Path of d,b; :: thesis: for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic
let C be Path of b,c; :: thesis: ((A + (- B)) + B) + C,A + C are_homotopic
A4: ((A + (- B)) + B) + C,A + (((- B) + B) + C) are_homotopic by A1, A2, A3, Th33;
set X = the constant Path of b,b;
( C,C are_homotopic & (- B) + B, the constant Path of b,b are_homotopic ) by A2, A3, BORSUK_2:12, BORSUK_6:86;
then A5: ((- B) + B) + C, the constant Path of b,b + C are_homotopic by A2, BORSUK_6:75;
the constant Path of b,b + C,C are_homotopic by A2, BORSUK_6:82;
then A6: ((- B) + B) + C,C are_homotopic by A5, BORSUK_6:79;
A,A are_homotopic by A1, BORSUK_2:12;
then A + (((- B) + B) + C),A + C are_homotopic by A1, A2, A6, BORSUK_6:75;
hence ((A + (- B)) + B) + C,A + C are_homotopic by A4, BORSUK_6:79; :: thesis: verum