let n be Element of NAT ; :: thesis: TOP-REAL n is arcwise_connected
set T = TOP-REAL n;
let a, b be Point of (TOP-REAL n); :: according to BORSUK_2:def 3 :: thesis: a,b are_connected
set L = LSeg a,b;

per cases ( a <> b or a = b ) ;

suppose a <> b ; :: thesis: a,b are_connected

then consider f being Function of I[01] ,((TOP-REAL n) | (LSeg a,b)) such that
A1: ( ( for x being Real st x in [.0 ,1.] holds
f . x = ((1 - x) * a) + (x * b) ) & f is being_homeomorphism & f . 0 = a & f . 1 = b ) by Th4;
A2: f is continuous by A1, TOPS_2:def 5;
A3: dom f = the carrier of I[01] by FUNCT_2:def 1;
rng f c= [#] ((TOP-REAL n) | (LSeg a,b)) ;
then rng f c= LSeg a,b by PRE_TOPC:def 10;
then rng f c= the carrier of (TOP-REAL n) by XBOOLE_1:1;
then reconsider g = f as Function of I[01] ,(TOP-REAL n) by A3, FUNCT_2:def 1, RELSET_1:11;
g is continuous by A2, PRE_TOPC:56;
hence a,b are_connected by A1, BORSUK_2:def 1; :: thesis: verum

end;

suppose a = b ; :: thesis: a,b are_connected

hence a,b are_connected ; :: thesis: verum

end;

end;