let X be Subset of REAL; :: thesis: ( X is real-bounded & X is closed implies X is compact )
assume that
A1: X is real-bounded and
A2: X is closed ; :: thesis: X is compact

now :: thesis: for s1 being Real_Sequence st rng s1 c= X holds
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X )

let s1 be Real_Sequence; :: thesis: ( rng s1 c= X implies ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) )
assume A3: rng s1 c= X ; :: thesis: ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X )
A4: s1 is bounded_below

proof

consider p being Real such that
A5: p is LowerBound of X by A1, XXREAL_2:def 9;
A6: for q being Real st q in X holds
p <= q by A5, XXREAL_2:def 2;
take r = p - 1; :: according to SEQ_2:def 4 :: thesis: for b₁ being set holds not s1 . b₁ <= r
A7: r + 1 = p - (1 - 1) ;
A8: for t being Real st t in rng s1 holds
r < t

proof

let t be Real; :: thesis: ( t in rng s1 implies r < t )
assume t in rng s1 ; :: thesis: r < t
then A9: p <= t by A3, A6;
r < p by A7, XREAL_1:29;
hence r < t by A9, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds r < s1 . n

proof

let n be Nat; :: thesis: r < s1 . n
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 3;
hence r < s1 . n by A8; :: thesis: verum

end;

hence for b₁ being set holds not s1 . b₁ <= r ; :: thesis: verum

end;

s1 is bounded_above

proof

consider p being Real such that
A10: p is UpperBound of X by A1, XXREAL_2:def 10;
A11: for q being Real st q in X holds
q <= p by A10, XXREAL_2:def 1;
take r = p + 1; :: according to SEQ_2:def 3 :: thesis: for b₁ being set holds not r <= s1 . b₁
A12: for t being Real st t in rng s1 holds
t < r

proof

let t be Real; :: thesis: ( t in rng s1 implies t < r )
assume t in rng s1 ; :: thesis: t < r
then A13: t <= p by A3, A11;
p < r by XREAL_1:29;
hence t < r by A13, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds s1 . n < r

proof

let n be Nat; :: thesis: s1 . n < r
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 3;
hence s1 . n < r by A12; :: thesis: verum

end;

hence for b₁ being set holds not r <= s1 . b₁ ; :: thesis: verum

end;

then s1 is bounded by A4;
then consider s2 being Real_Sequence such that
A14: s2 is subsequence of s1 and
A15: s2 is convergent by SEQ_4:40;
ex Nseq being increasing sequence of NAT st s2 = s1 * Nseq by A14, VALUED_0:def 17;
then rng s2 c= rng s1 by RELAT_1:26;
then rng s2 c= X by A3;
then lim s2 in X by A2, A15;
hence ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A14, A15; :: thesis: verum

end;

hence X is compact ; :: thesis: verum