let a, b be Point of R^1 ; BORSUK_2:def 3 a,b are_connected
per cases
( a <= b or b <= a )
;
suppose A1:
a <= b
;
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;
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
;
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] ,
(R^1 | 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 reconsider B =
[.b,a.] as
Subset of
R^1 by TOPMETR:24;
b in B
by A3, XXREAL_1:1;
then reconsider B =
[.b,a.] as non
empty Subset of
R^1 ;
A4:
Closed-Interval-TSpace b,
a = R^1 | B
by A3, TOPMETR:26;
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 A4, FUNCT_2:9, TOPMETR:27;
reconsider g =
g as
Function of
I[01] ,
R^1 ;
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] ,
(R^1 | 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, BORSUK_2:def 1;
then reconsider P =
g as
Path of
b,
a by A7, A5, A6, BORSUK_2:def 2;
take h =
- P;
BORSUK_2:def 1 ( 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, A5, A6, 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;
verum end;