let X be non empty TopSpace; 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; ( 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
; 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; 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; ( C + A,C + B are_homotopic implies A,B are_homotopic )
A3:
((- C) + C) + A,(- C) + (C + A) are_homotopic
by A1, A2, BORSUK_6:73;
assume A4:
C + A,C + B are_homotopic
; A,B are_homotopic
( b,c are_connected & - C, - C are_homotopic )
by A1, A2, BORSUK_2:12, BORSUK_6:42;
then
(- C) + (C + A),(- C) + (C + B) are_homotopic
by A2, A4, BORSUK_6:75;
then A5:
((- C) + C) + A,(- C) + (C + B) are_homotopic
by A3, BORSUK_6:79;
((- C) + C) + B,(- C) + (C + B) are_homotopic
by A1, A2, BORSUK_6:73;
then A6:
((- C) + C) + A,((- C) + C) + B are_homotopic
by A5, BORSUK_6:79;
((- C) + C) + A,A are_homotopic
by A1, A2, Th23, BORSUK_2:12;
then A7:
A,((- C) + C) + B are_homotopic
by A6, BORSUK_6:79;
((- C) + C) + B,B are_homotopic
by A1, A2, Th23, BORSUK_2:12;
hence
A,B are_homotopic
by A7, BORSUK_6:79; verum