let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n) holds LSeg p1,p2 is compact
let p1, p2 be Point of (TOP-REAL n); :: thesis: LSeg p1,p2 is compact
set P = LSeg p1,p2;
set T = (TOP-REAL n) | (LSeg p1,p2);

now

per cases ( p1 = p2 or p1 <> p2 ) ;

suppose p1 = p2 ; :: thesis: (TOP-REAL n) | (LSeg p1,p2) is compact

then LSeg p1,p2 = {p1} by RLTOPSP1:71;
then A1: {p1} = [#] ((TOP-REAL n) | (LSeg p1,p2)) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL n) | (LSeg p1,p2)) ;
then Sspace p1 = (TOP-REAL n) | (LSeg p1,p2) by TEX_2:def 4;
then (TOP-REAL n) | (LSeg p1,p2) = 1TopSp {p1} by A1, TDLAT_3:def 1;
hence (TOP-REAL n) | (LSeg p1,p2) is compact by PCOMPS_1:9; :: thesis: verum

end;

suppose p1 <> p2 ; :: thesis: (TOP-REAL n) | (LSeg p1,p2) is compact

then LSeg p1,p2 is_an_arc_of p1,p2 by TOPREAL1:15;
then consider f being Function of I[01] ,((TOP-REAL n) | (LSeg p1,p2)) such that
A2: f is being_homeomorphism and
( f . 0 = p1 & f . 1 = p2 ) by TOPREAL1:def 2;
A3: f is continuous by A2, TOPS_2:def 5;
A4: I[01] is compact by HEINE:11, TOPMETR:27;
rng f = [#] ((TOP-REAL n) | (LSeg p1,p2)) by A2, TOPS_2:def 5;
hence (TOP-REAL n) | (LSeg p1,p2) is compact by A3, A4, COMPTS_1:23; :: thesis: verum

end;

end;

end;

hence LSeg p1,p2 is compact by COMPTS_1:12; :: thesis: verum