let s, g be real number ; :: thesis: [.s,g.] is compact
for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] )

proof

let s1 be Real_Sequence; :: thesis: ( rng s1 c= [.s,g.] implies ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) )
A1: [.s,g.] is closed by Th23;
assume A2: rng s1 c= [.s,g.] ; :: thesis: ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] )
then consider s2 being Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent by Th22, SEQ_4:57;
take s2 ; :: thesis: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] )
ex Nseq being increasing sequence of NAT st s2 = s1 * Nseq by A3, VALUED_0:def 17;
then rng s2 c= rng s1 by RELAT_1:45;
then rng s2 c= [.s,g.] by A2, XBOOLE_1:1;
hence ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) by A3, A4, A1, Def4; :: thesis: verum

end;

hence [.s,g.] is compact by Def3; :: thesis: verum