set P = LSeg (p1,p2);
set T = (TOP-REAL n) | (LSeg (p1,p2));

now :: thesis: (TOP-REAL n) | (LSeg (p1,p2)) is compact

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:70;
then A1: {p1} = [#] ((TOP-REAL n) | (LSeg (p1,p2))) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ;
then Sspace p1 = (TOP-REAL n) | (LSeg (p1,p2)) by TEX_2:def 2;
then (TOP-REAL n) | (LSeg (p1,p2)) = 1TopSp {p1} by A1, TDLAT_3:def 1;
hence (TOP-REAL n) | (LSeg (p1,p2)) is compact ; :: 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:9;
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 and
f . 1 = p2 ;
A3: I[01] is compact by HEINE:4, TOPMETR:20;
( f is continuous & 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, COMPTS_1:14; :: thesis: verum

end;

end;

end;

hence LSeg (p1,p2) is compact by COMPTS_1:3; :: thesis: verum