let a, b be Point of R^1 ; :: 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 reconsider B =
[.a,b.] as
Subset of
R^1 by TOPMETR:24;
reconsider B =
B as non
empty Subset of
R^1 by A1, XXREAL_1:1;
A2:
Closed-Interval-TSpace a,
b = R^1 | B
by A1, TOPMETR:26;
then A3:
L[01] ((#) a,b),
(a,b (#) ) is
continuous Function of
I[01] ,
(R^1 | B)
by A1, TOPMETR:27, TREAL_1:11;
the
carrier of
(R^1 | B) c= the
carrier of
R^1
by BORSUK_1:35;
then reconsider g =
L[01] ((#) a,b),
(a,b (#) ) as
Function of the
carrier of
I[01] ,the
carrier of
R^1 by A2, FUNCT_2:9, TOPMETR:27;
reconsider g =
g as
Function of
I[01] ,
R^1 ;
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 reconsider B =
[.b,a.] as
Subset of
R^1 by TOPMETR:24;
b in B
by A4, XXREAL_1:1;
then reconsider B =
[.b,a.] as non
empty Subset of
R^1 ;
A5:
Closed-Interval-TSpace b,
a = R^1 | B
by A4, TOPMETR:26;
then A6:
L[01] ((#) b,a),
(b,a (#) ) is
continuous Function of
I[01] ,
(R^1 | B)
by A4, TOPMETR:27, TREAL_1:11;
the
carrier of
(R^1 | B) c= the
carrier of
R^1
by BORSUK_1:35;
then reconsider g =
L[01] ((#) b,a),
(b,a (#) ) as
Function of the
carrier of
I[01] ,the
carrier of
R^1 by A5, FUNCT_2:9, TOPMETR:27;
reconsider g =
g as
Function of
I[01] ,
R^1 ;
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, BORSUK_2:def 1;
then reconsider P =
g as
Path of
b,
a by A7, A8, A9, BORSUK_2:def 2;
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] ,
R^1 st
(
t is
continuous &
t . 0 = a &
t . 1
= b )
by A7, A8, A9, BORSUK_2:18;
then
a,
b are_connected
by BORSUK_2:def 1;
hence
(
h is
continuous &
h . 0 = a &
h . 1
= b )
by BORSUK_2:def 2;
:: thesis: verum end;