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:83, XXREAL_1:1, XXREAL_2:def 12;
(
0 <= a &
b <= 1 )
by BORSUK_1:86;
then A2:
Closed-Interval-TSpace a,
b = I[01] | B
by A1, TOPMETR:31;
then A3:
L[01] ((#) a,b),
(a,b (#) ) is
continuous Function of
I[01] ,
(I[01] | B)
by A1, TOPMETR:27, TREAL_1:11;
the
carrier of
(I[01] | B) c= the
carrier of
I[01]
by BORSUK_1:35;
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:9, TOPMETR:27;
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 A3, PRE_TOPC:56;
:: thesis: ( g . 0 = a & g . 1 = b )
0 = (#) 0 ,1
by TREAL_1:def 1;
hence g . 0 =
(#) a,
b
by A1, TREAL_1:12
.=
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:12
.=
b
by A1, TREAL_1:def 2
;
:: thesis: verum end; suppose A4:
b <= a
;
:: thesis: a,b are_connected then reconsider B =
[.b,a.] as non
empty Subset of
I[01] by BORSUK_1:83, XXREAL_1:1, XXREAL_2:def 12;
(
0 <= b &
a <= 1 )
by BORSUK_1:86;
then A5:
Closed-Interval-TSpace b,
a = I[01] | B
by A4, TOPMETR:31;
then A6:
L[01] ((#) b,a),
(b,a (#) ) is
continuous Function of
I[01] ,
(I[01] | B)
by A4, TOPMETR:27, TREAL_1:11;
the
carrier of
(I[01] | B) c= the
carrier of
I[01]
by BORSUK_1:35;
then reconsider g =
L[01] ((#) b,a),
(b,a (#) ) as
Function of the
carrier of
I[01] ,the
carrier of
I[01] by A5, FUNCT_2:9, TOPMETR:27;
reconsider g =
g as
Function of
I[01] ,
I[01] ;
A7:
g is
continuous
by A6, PRE_TOPC:56;
0 = (#) 0 ,1
by TREAL_1:def 1;
then A8:
g . 0 =
(#) b,
a
by A4, TREAL_1:12
.=
b
by A4, TREAL_1:def 1
;
1
= 0 ,1
(#)
by TREAL_1:def 2;
then A9:
g . 1 =
b,
a (#)
by A4, TREAL_1:12
.=
a
by A4, TREAL_1:def 2
;
then
b,
a are_connected
by A7, A8, Def1;
then reconsider P =
g as
Path of
b,
a by A7, A8, A9, Def2;
take h =
- P;
:: according to BORSUK_2:def 1 :: thesis: ( h is continuous & h . 0 = a & h . 1 = b )
ex
t being
Function of
I[01] ,
I[01] st
(
t is
continuous &
t . 0 = a &
t . 1
= b )
by A7, A8, A9, Th18;
then
a,
b are_connected
by Def1;
hence
(
h is
continuous &
h . 0 = a &
h . 1
= b )
by Def2;
:: thesis: verum end;