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 )
;

end;

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;( 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

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;( 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