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:17;
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:19;
the
carrier of
(R^1 | B) c= the
carrier of
R^1
by BORSUK_1:1;
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:7, TOPMETR:20;
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:20, TREAL_1:8;
hence
g is
continuous
by PRE_TOPC:26;
( 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
;
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
;
verum end; suppose A3:
b <= a
;
a,b are_connected reconsider B =
[.b,a.] as
Subset of
R^1 by TOPMETR:17;
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:19;
the
carrier of
(R^1 | B) c= the
carrier of
R^1
by BORSUK_1:1;
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:7, TOPMETR:20;
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: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
;
L[01] (
((#) (b,a)),
((b,a) (#))) is
continuous Function of
I[01],
(R^1 | B)
by A3, A4, TOPMETR:20, TREAL_1:8;
then A7:
g is
continuous
by PRE_TOPC:26;
then
b,
a are_connected
by A5, A6;
then reconsider P =
g as
Path of
b,
a by A7, A5, A6, BORSUK_2:def 2;
take
- P
;
BORSUK_2:def 1 ( - P is continuous & (- P) . 0 = a & (- P) . 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:15;
then
a,
b are_connected
;
hence
(
- P is
continuous &
(- P) . 0 = a &
(- P) . 1
= b )
by BORSUK_2:def 2;
verum end;