let a, b be Point of I[01]; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected

per cases ( a <= b or b <= a ) ;

suppose A1: a <= b ; :: thesis: a,b are_connected

then reconsider B = [.a,b.] as non empty Subset of I[01] by BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
( 0 <= a & b <= 1 ) by BORSUK_1:43;
then A2: Closed-Interval-TSpace (a,b) = I[01] | B by A1, TOPMETR:24;
the carrier of (I[01] | B) c= the carrier of I[01] by BORSUK_1:1;
then reconsider g = L[01] (((#) (a,b)),((a,b) (#))) as Function of the carrier of I[01], the carrier of I[01] by A2, FUNCT_2:7, TOPMETR:20;
reconsider g = g as Function of I[01],I[01] ;
take g ; :: according to BORSUK_2:def 1 :: thesis: ( g is continuous & g . 0 = a & g . 1 = b )
thus g is continuous by A1, A2, PRE_TOPC:26, TOPMETR:20, TREAL_1:8; :: thesis: ( g . 0 = a & g . 1 = b )
0 = (#) (0,1) by TREAL_1:def 1;
hence g . 0 = (#) (a,b) by A1, TREAL_1:9
.= a by A1, TREAL_1:def 1 ;
:: thesis: g . 1 = b
1 = (0,1) (#) by TREAL_1:def 2;
hence g . 1 = (a,b) (#) by A1, TREAL_1:9
.= b by A1, TREAL_1:def 2 ;
:: thesis: verum

end;

suppose A3: b <= a ; :: thesis: a,b are_connected

then reconsider B = [.b,a.] as non empty Subset of I[01] by BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
( 0 <= b & a <= 1 ) by BORSUK_1:43;
then A4: Closed-Interval-TSpace (b,a) = I[01] | B by A3, TOPMETR:24;
the carrier of (I[01] | B) c= the carrier of I[01] by BORSUK_1:1;
then reconsider g = L[01] (((#) (b,a)),((b,a) (#))) as Function of the carrier of I[01], the carrier of I[01] by A4, FUNCT_2:7, TOPMETR:20;
reconsider g = g as Function of I[01],I[01] ;
0 = (#) (0,1) by TREAL_1:def 1;
then A5: g . 0 = (#) (b,a) by A3, TREAL_1:9
.= b by A3, TREAL_1:def 1 ;
1 = (0,1) (#) by TREAL_1:def 2;
then A6: g . 1 = (b,a) (#) by A3, TREAL_1:9
.= a by A3, TREAL_1:def 2 ;
A7: g is continuous by A3, A4, PRE_TOPC:26, TOPMETR:20, TREAL_1:8;
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[01],I[01] 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;