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