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 A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
let a, b, c be Point of X; :: thesis: ( a,b are_connected & c,b are_connected implies for A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic )
assume that
A1: a,b are_connected and
A2: c,b are_connected ; :: thesis: for A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
let A1, A2 be Path of a,b; :: thesis: for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
let B be Path of c,b; :: thesis: ( A1,A2 are_homotopic implies A1,(A2 + (- B)) + B are_homotopic )
consider X being constant Path of b,b;
assume A3: A1,A2 are_homotopic ; :: thesis: A1,(A2 + (- B)) + B are_homotopic
(- B) + B,X are_homotopic by A2, BORSUK_6:94;
then A4: A2 + ((- B) + B),A1 + X are_homotopic by A1, A3, BORSUK_6:83;
A1,A1 + X are_homotopic by A1, BORSUK_6:88;
then A5: A2 + ((- B) + B),A1 are_homotopic by A4, BORSUK_6:87;
A2 + ((- B) + B),(A2 + (- B)) + B are_homotopic by A1, A2, BORSUK_6:81;
hence A1,(A2 + (- B)) + B are_homotopic by A5, BORSUK_6:87; :: thesis: verum