let P be Subset of (TOP-REAL n); :: thesis: ( 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 ; :: according to JORDAN1:def 1 :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence P is connected by Th2; :: thesis: verum