let X be non empty TopSpace; :: thesis: for a, b, c being Point of X st a,b are_connected & c,b are_connected holds
for A, B being Path of a,b
for C being Path of b,c st A + C,B + C are_homotopic holds
A,B are_homotopic
let a, b, c be Point of X; :: thesis: ( a,b are_connected & c,b are_connected implies for A, B being Path of a,b
for C being Path of b,c st A + C,B + C are_homotopic holds
A,B are_homotopic )
assume that
A1: a,b are_connected and
A2: c,b are_connected ; :: thesis: for A, B being Path of a,b
for C being Path of b,c st A + C,B + C are_homotopic holds
A,B are_homotopic
let A, B be Path of a,b; :: thesis: for C being Path of b,c st A + C,B + C are_homotopic holds
A,B are_homotopic
let C be Path of b,c; :: thesis: ( A + C,B + C are_homotopic implies A,B are_homotopic )
A3: (A + C) + (- C),A are_homotopic by A1, A2, Th19, BORSUK_2:12;
assume A4: A + C,B + C are_homotopic ; :: thesis: A,B are_homotopic
( a,c are_connected & - C, - C are_homotopic ) by A1, A2, BORSUK_2:12, BORSUK_6:42;
then (A + C) + (- C),(B + C) + (- C) are_homotopic by A2, A4, BORSUK_6:75;
then A5: A,(B + C) + (- C) are_homotopic by A3, BORSUK_6:79;
(B + C) + (- C),B are_homotopic by A1, A2, Th19, BORSUK_2:12;
hence A,B are_homotopic by A5, BORSUK_6:79; :: thesis: verum