let n be Nat; :: thesis: TOP-REAL n is pathwise_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
for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * a) + (x * b) and
A1: f is being_homeomorphism and
A2: ( f . 0 = a & f . 1 = b ) by Th3;
rng f c= [#] ((TOP-REAL n) | (LSeg (a,b))) ;
then rng f c= LSeg (a,b) by PRE_TOPC:def 5;
then ( dom f = the carrier of I[01] & rng f c= the carrier of (TOP-REAL n) ) by FUNCT_2:def 1, XBOOLE_1:1;
then reconsider g = f as Function of I[01],(TOP-REAL n) by RELSET_1:4;
f is continuous by A1, TOPS_2:def 5;
then g is continuous by PRE_TOPC:26;
hence a,b are_connected by A2; :: thesis: verum

end;

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

hence a,b are_connected ; :: thesis: verum

end;

end;