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 & a,c are_connected ) and
A2: 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
A3: (((A + (- A)) + C) + B) + (- B),C are_homotopic by A1, A2, Th39;
A4: - B, - B are_homotopic by A2, BORSUK_2:12;
( A + (((- A) + C) + B),((A + (- A)) + C) + B are_homotopic & a,d are_connected ) by A1, A2, Th33, BORSUK_6:42;
then (A + (((- A) + C) + B)) + (- B),(((A + (- A)) + C) + B) + (- B) are_homotopic by A2, A4, BORSUK_6:75;
hence (A + (((- A) + C) + B)) + (- B),C are_homotopic by A3, BORSUK_6:79; :: thesis: verum