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 & d,c 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 & d,c 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: d,c 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: A + (((- A) + C) + B),((A + (- A)) + C) + B are_homotopic by A1, A2, A3, Th34;
A5: a,d are_connected by A2, A3, BORSUK_6:46;
- B, - B are_homotopic by A3, BORSUK_2:15;
then A6: (A + (((- A) + C) + B)) + (- B),(((A + (- A)) + C) + B) + (- B) are_homotopic by A3, A4, A5, BORSUK_6:83;
(((A + (- A)) + C) + B) + (- B),C are_homotopic by A1, A2, A3, Th40;
hence (A + (((- A) + C) + B)) + (- B),C are_homotopic by A6, BORSUK_6:87; :: thesis: verum