let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds
P is compact
let p, q be Point of (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds
P is compact
let P be Subset of (TOP-REAL n); :: thesis: ( P is_an_arc_of p,q implies P is compact )
assume P is_an_arc_of p,q ; :: thesis: P is compact
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A1: f is being_homeomorphism and
f . 0 = p and
f . 1 = q by TOPREAL1:def 1;

per cases ( P <> {} or P = {} (TOP-REAL n) ) ;

suppose P <> {} ; :: thesis: P is compact

then reconsider P9 = P as non empty Subset of (TOP-REAL n) ;
( f is continuous & rng f = [#] ((TOP-REAL n) | P9) ) by A1, TOPS_2:def 5;
then (TOP-REAL n) | P9 is compact by COMPTS_1:14;
hence P is compact by COMPTS_1:3; :: thesis: verum

end;

suppose P = {} (TOP-REAL n) ; :: thesis: P is compact

hence P is compact ; :: thesis: verum

end;

end;