let s, g be Real; :: 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 Th5;
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 Th4, SEQ_4:40;
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:26;
then rng s2 c= [.s,g.] by A2;
hence ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) by A3, A4, A1; :: thesis: verum

end;

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