let T be non empty pathwise_connected TopSpace; for a1, b1, c1, d1, e1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic
let a1, b1, c1, d1, e1 be Point of T; for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic
A1:
( c1,d1 are_connected & d1,e1 are_connected )
by BORSUK_2:def 3;
( a1,b1 are_connected & b1,c1 are_connected )
by BORSUK_2:def 3;
hence
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic
by A1, Th35; verum