let X be non empty TopSpace; :: thesis: for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & c,d are_connected holds
for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic
let a, b, c, d be Point of X; :: thesis: ( a,b are_connected & a,c are_connected & c,d are_connected implies for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic )
assume that
A1: a,b are_connected and
A2: a,c are_connected and
A3: c,d are_connected ; :: thesis: for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic
let A be Path of a,b; :: thesis: for B being Path of c,d
for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic
let B be Path of c,d; :: thesis: for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic
let C be Path of a,c; :: thesis: (((A + (- A)) + C) + B) + (- B),C are_homotopic
A4: B + (- B),B + (- B) are_homotopic by BORSUK_2:15;
(A + (- A)) + C,C are_homotopic by A1, A2, Th26, BORSUK_2:15;
then A5: ((A + (- A)) + C) + (B + (- B)),C + (B + (- B)) are_homotopic by A2, A4, BORSUK_6:83;
(((A + (- A)) + C) + B) + (- B),((A + (- A)) + C) + (B + (- B)) are_homotopic by A2, A3, BORSUK_6:81;
then A6: (((A + (- A)) + C) + B) + (- B),C + (B + (- B)) are_homotopic by A5, BORSUK_6:87;
A7: C,(C + B) + (- B) are_homotopic by A2, A3, Th20, BORSUK_2:15;
(C + B) + (- B),C + (B + (- B)) are_homotopic by A2, A3, BORSUK_6:81;
then C,C + (B + (- B)) are_homotopic by A7, BORSUK_6:87;
hence (((A + (- A)) + C) + B) + (- B),C are_homotopic by A6, BORSUK_6:87; :: thesis: verum