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

end;

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