let P be Subset of (TOP-REAL n); ( P is convex implies P is connected )
assume A1:
for w3, w4 being Point of (TOP-REAL n) st w3 in P & w4 in P holds
LSeg (w3,w4) c= P
; JORDAN1:def 1 P is connected
for w1, w2 being Point of (TOP-REAL n) st w1 in P & w2 in P & w1 <> w2 holds
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w2 = h . 1 )
proof
let w1,
w2 be
Point of
(TOP-REAL n);
( w1 in P & w2 in P & w1 <> w2 implies ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w2 = h . 1 ) )
assume that A2:
w1 in P
and A3:
w2 in P
and A4:
w1 <> w2
;
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w2 = h . 1 )
A5:
LSeg (
w1,
w2)
c= P
by A1, A2, A3;
LSeg (
w1,
w2)
is_an_arc_of w1,
w2
by A4, TOPREAL1:9;
then consider f being
Function of
I[01],
((TOP-REAL n) | (LSeg (w1,w2))) such that A6:
f is
being_homeomorphism
and A7:
f . 0 = w1
and A8:
f . 1
= w2
by TOPREAL1:def 1;
A9:
f is
continuous
by A6, TOPS_2:def 5;
A10:
rng f = [#] ((TOP-REAL n) | (LSeg (w1,w2)))
by A6, TOPS_2:def 5;
then A11:
rng f c= P
by A5, PRE_TOPC:def 5;
then
[#] ((TOP-REAL n) | (LSeg (w1,w2))) c= [#] ((TOP-REAL n) | P)
by A10, PRE_TOPC:def 5;
then A12:
(TOP-REAL n) | (LSeg (w1,w2)) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:3;
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then reconsider g =
f as
Function of
[.0,1.],
P by A11, FUNCT_2:2;
the
carrier of
((TOP-REAL n) | P) =
[#] ((TOP-REAL n) | P)
.=
P
by PRE_TOPC:def 5
;
then reconsider gt =
g as
Function of
I[01],
((TOP-REAL n) | P) by BORSUK_1:40;
gt is
continuous
by A9, A12, PRE_TOPC:26;
hence
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w2 = h . 1 )
by A7, A8;
verum
end;
hence
P is connected
by Th2; verum