let a, b be Point of I; :: according to BORSUK_2:def 3 :: thesis:
per cases ( a <= b or b <= a ) ;
suppose A1: a <= b ; :: thesis:
then reconsider B = [.a,b.] as non empty Subset of I by ;
( 0 <= a & b <= 1 ) by BORSUK_1:43;
then A2: Closed-Interval-TSpace (a,b) = I | B by ;
the carrier of () c= the carrier of I by BORSUK_1:1;
then reconsider g = L (((#) (a,b)),((a,b) (#))) as Function of the carrier of I, the carrier of I by ;
reconsider g = g as Function of I,I ;
take g ; :: according to BORSUK_2:def 1 :: thesis: ( g is continuous & g . 0 = a & g . 1 = b )
thus g is continuous by ; :: thesis: ( g . 0 = a & g . 1 = b )
0 = (#) (0,1) by TREAL_1:def 1;
hence g . 0 = (#) (a,b) by
.= a by ;
:: thesis: g . 1 = b
1 = (0,1) (#) by TREAL_1:def 2;
hence g . 1 = (a,b) (#) by
.= b by ;
:: thesis: verum
end;
suppose A3: b <= a ; :: thesis:
then reconsider B = [.b,a.] as non empty Subset of I by ;
( 0 <= b & a <= 1 ) by BORSUK_1:43;
then A4: Closed-Interval-TSpace (b,a) = I | B by ;
the carrier of () c= the carrier of I by BORSUK_1:1;
then reconsider g = L (((#) (b,a)),((b,a) (#))) as Function of the carrier of I, the carrier of I by ;
reconsider g = g as Function of I,I ;
0 = (#) (0,1) by TREAL_1:def 1;
then A5: g . 0 = (#) (b,a) by
.= b by ;
1 = (0,1) (#) by TREAL_1:def 2;
then A6: g . 1 = (b,a) (#) by
.= a by ;
A7: g is continuous by ;
then b,a are_connected by A5, A6;
then reconsider P = g as Path of b,a by A7, A5, A6, Def2;
take - P ; :: according to BORSUK_2:def 1 :: thesis: ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b )
ex t being Function of I,I st
( t is continuous & t . 0 = a & t . 1 = b ) by A7, A5, A6, Th13;
then a,b are_connected ;
hence ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b ) by Def2; :: thesis: verum
end;
end;