let X be non empty TopSpace; 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; ( 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
; 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; 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; for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic
let C be Path of a,c; (((A + (- A)) + C) + B) + (- B),C are_homotopic
( B + (- B),B + (- B) are_homotopic & (A + (- A)) + C,C are_homotopic )
by A1, A2, Th25, BORSUK_2:12;
then A4:
((A + (- A)) + C) + (B + (- B)),C + (B + (- B)) are_homotopic
by A2, BORSUK_6:75;
( C,(C + B) + (- B) are_homotopic & (C + B) + (- B),C + (B + (- B)) are_homotopic )
by A2, A3, Th19, BORSUK_2:12, BORSUK_6:73;
then A5:
C,C + (B + (- B)) are_homotopic
by BORSUK_6:79;
(((A + (- A)) + C) + B) + (- B),((A + (- A)) + C) + (B + (- B)) are_homotopic
by A2, A3, BORSUK_6:73;
then
(((A + (- A)) + C) + B) + (- B),C + (B + (- B)) are_homotopic
by A4, BORSUK_6:79;
hence
(((A + (- A)) + C) + B) + (- B),C are_homotopic
by A5, BORSUK_6:79; verum