let a, b be Point of I[01] ; BORSUK_2:def 3 a,b are_connected
per cases
( a <= b or b <= a )
;
suppose A1:
a <= b
;
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;
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
;
BORSUK_2:def 1 ( g is continuous & g . 0 = a & g . 1 = b )
L[01] ((#) a,b),
(a,b (#) ) is
continuous Function of
I[01] ,
(I[01] | B)
by A1, A2, TOPMETR:27, TREAL_1:11;
hence
g is
continuous
by PRE_TOPC:56;
( 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
;
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
;
verum end; suppose A3:
b <= a
;
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 A4:
Closed-Interval-TSpace b,
a = I[01] | B
by A3, TOPMETR:31;
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 A4, FUNCT_2:9, TOPMETR:27;
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:12
.=
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:12
.=
a
by A3, TREAL_1:def 2
;
L[01] ((#) b,a),
(b,a (#) ) is
continuous Function of
I[01] ,
(I[01] | B)
by A3, A4, TOPMETR:27, TREAL_1:11;
then A7:
g is
continuous
by PRE_TOPC:56;
then
b,
a are_connected
by A5, A6, Def1;
then reconsider P =
g as
Path of
b,
a by A7, A5, A6, Def2;
take h =
- P;
BORSUK_2:def 1 ( 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, A5, A6, Th18;
then
a,
b are_connected
by Def1;
hence
(
h is
continuous &
h . 0 = a &
h . 1
= b )
by Def2;
verum end;