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

now

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 number such that
B5: p is LowerBound of X by A1, XXREAL_2:def 9;
A5: for q being real number st q in X holds
p <= q by B5, XXREAL_2:def 2;
take r = p - 1; :: according to SEQ_2:def 4 :: thesis: for b₁ being Element of NAT holds not s1 . b₁ <= r
A6: r + 1 = p - (1 - 1) ;
A7: for t being real number st t in rng s1 holds
r < t

proof

let t be real number ; :: thesis: ( t in rng s1 implies r < t )
assume t in rng s1 ; :: thesis: r < t
then A8: p <= t by A3, A5;
r < p by A6, XREAL_1:31;
hence r < t by A8, XXREAL_0:2; :: thesis: verum

end;

for n being Element of NAT holds r < s1 . n

proof

let n be Element of NAT ; :: thesis: r < s1 . n
n in NAT ;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 5;
hence r < s1 . n by A7; :: thesis: verum

end;

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

end;

s1 is bounded_above

proof

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

proof

let t be real number ; :: thesis: ( t in rng s1 implies t < r )
assume t in rng s1 ; :: thesis: t < r
then A11: t <= p by A3, A9;
p < r by XREAL_1:31;
hence t < r by A11, XXREAL_0:2; :: thesis: verum

end;

for n being Element of NAT holds s1 . n < r

proof

let n be Element of NAT ; :: thesis: s1 . n < r
n in NAT ;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 5;
hence s1 . n < r by A10; :: thesis: verum

end;

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

end;

then s1 is bounded by A4, SEQ_2:def 8;
then consider s2 being Real_Sequence such that
A12: s2 is subsequence of s1 and
A13: s2 is convergent by SEQ_4:57;
ex Nseq being increasing sequence of NAT st s2 = s1 * Nseq by A12, VALUED_0:def 17;
then rng s2 c= rng s1 by RELAT_1:45;
then rng s2 c= X by A3, XBOOLE_1:1;
then lim s2 in X by A2, A13, Def4;
hence ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A12, A13; :: thesis: verum

end;

hence X is compact by Def3; :: thesis: verum