let X be non empty TopSpace; :: thesis: for a, b, c being Point of X st a,b are_connected & a,c are_connected holds
for A, B being Path of a,b
for C being Path of c,a st C + A,C + B are_homotopic holds
A,B are_homotopic
let a, b, c be Point of X; :: thesis: ( a,b are_connected & a,c are_connected implies for A, B being Path of a,b
for C being Path of c,a st C + A,C + B are_homotopic holds
A,B are_homotopic )
assume that
A1: a,b are_connected and
A2: a,c are_connected ; :: thesis: for A, B being Path of a,b
for C being Path of c,a st C + A,C + B are_homotopic holds
A,B are_homotopic
let A, B be Path of a,b; :: thesis: for C being Path of c,a st C + A,C + B are_homotopic holds
A,B are_homotopic
let C be Path of c,a; :: thesis: ( C + A,C + B are_homotopic implies A,B are_homotopic )
assume A3: C + A,C + B are_homotopic ; :: thesis: A,B are_homotopic
consider X being constant Path of b,b;
A4: b,c are_connected by A1, A2, BORSUK_6:46;
- C, - C are_homotopic by A2, BORSUK_2:15;
then A5: (- C) + (C + A),(- C) + (C + B) are_homotopic by A2, A3, A4, BORSUK_6:83;
A6: ((- C) + C) + A,(- C) + (C + A) are_homotopic by A1, A2, BORSUK_6:81;
A7: ((- C) + C) + B,(- C) + (C + B) are_homotopic by A1, A2, BORSUK_6:81;
((- C) + C) + A,(- C) + (C + B) are_homotopic by A5, A6, BORSUK_6:87;
then A8: ((- C) + C) + A,((- C) + C) + B are_homotopic by A7, BORSUK_6:87;
((- C) + C) + A,A are_homotopic by A1, A2, Th24, BORSUK_2:15;
then A9: A,((- C) + C) + B are_homotopic by A8, BORSUK_6:87;
((- C) + C) + B,B are_homotopic by A1, A2, Th24, BORSUK_2:15;
hence A,B are_homotopic by A9, BORSUK_6:87; :: thesis: verum