let X be Subset of REAL ; :: thesis: ( X is compact implies X is bounded )
assume A1: X is compact ; :: thesis: X is bounded
assume A2: not X is bounded ; :: thesis: contradiction

now

per cases ( not X is bounded_above or not X is bounded_below ) by A2;

suppose A3: not X is bounded_above ; :: thesis: contradiction

defpred S₁[ Element of NAT , Element of REAL ] means ex q being real number st
( q = $2 & q in X & $1 < q );
A4: for n being Element of NAT ex p being Element of REAL st S₁[n,p]

proof

let n be Element of NAT ; :: thesis: ex p being Element of REAL st S₁[n,p]
consider t being real number such that
A5: ( t in X & n < t ) by A3, SEQ_4:def 1;
take t ; :: thesis: ( t is Element of REAL & S₁[n,t] )
thus ( t is Element of REAL & S₁[n,t] ) by A5; :: thesis: verum

end;

consider f being Function of NAT ,REAL such that
A6: for n being Element of NAT holds S₁[n,f . n] from FUNCT_2:sch 3(A4);

A7: now

let n be Element of NAT ; :: thesis: ( f . n in X & n < f . n )
ex q being real number st
( q = f . n & q in X & n < q ) by A6;
hence ( f . n in X & n < f . n ) ; :: thesis: verum

end;

A8: for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )

proof

let p be real number ; :: thesis: ( p in X implies ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) ) )
assume p in X ; :: thesis: ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider q being real number such that
A9: q = 1 ;
take r = q; :: thesis: ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider k being Element of NAT such that
A10: p + 1 < k by SEQ_4:10;
take n = k; :: thesis: ( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
thus 0 < r by A9; :: thesis: for m being Element of NAT st n < m holds
r < abs ((f . m) - p)
let m be Element of NAT ; :: thesis: ( n < m implies r < abs ((f . m) - p) )
assume n < m ; :: thesis: r < abs ((f . m) - p)
then p + 1 < m by A10, XXREAL_0:2;
then p + 1 < f . m by A7, XXREAL_0:2;
then 1 < (f . m) - p by XREAL_1:22;
hence r < abs ((f . m) - p) by A9, ABSVALUE:def 1; :: thesis: verum

end;

rng f c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in X )
assume x in rng f ; :: thesis: x in X
then consider y being set such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A11, FUNCT_2:def 1;
f . y in X by A7;
hence x in X by A12; :: thesis: verum

end;

then ex s2 being Real_Sequence st
( s2 is subsequence of f & s2 is convergent & lim s2 in X ) by A1, Def3;
hence contradiction by A8, Th27; :: thesis: verum

end;

suppose A13: not X is bounded_below ; :: thesis: contradiction

defpred S₁[ Element of NAT , Element of REAL ] means ex q being real number st
( q = $2 & q in X & q < - $1 );
A14: for n being Element of NAT ex p being Element of REAL st S₁[n,p]

proof

let n be Element of NAT ; :: thesis: ex p being Element of REAL st S₁[n,p]
consider t being real number such that
A15: ( t in X & t < - n ) by A13, SEQ_4:def 2;
take t ; :: thesis: ( t is Element of REAL & S₁[n,t] )
thus ( t is Element of REAL & S₁[n,t] ) by A15; :: thesis: verum

end;

consider f being Function of NAT ,REAL such that
A16: for n being Element of NAT holds S₁[n,f . n] from FUNCT_2:sch 3(A14);

A17: now

let n be Element of NAT ; :: thesis: ( f . n in X & f . n < - n )
ex q being real number st
( q = f . n & q in X & q < - n ) by A16;
hence ( f . n in X & f . n < - n ) ; :: thesis: verum

end;

A18: for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )

proof

let p be real number ; :: thesis: ( p in X implies ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) ) )
assume p in X ; :: thesis: ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider q being real number such that
A19: q = 1 ;
take r = q; :: thesis: ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider k being Element of NAT such that
A20: abs (p - 1) < k by SEQ_4:10;
take n = k; :: thesis: ( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
thus 0 < r by A19; :: thesis: for m being Element of NAT st n < m holds
r < abs ((f . m) - p)
let m be Element of NAT ; :: thesis: ( n < m implies r < abs ((f . m) - p) )
assume n < m ; :: thesis: r < abs ((f . m) - p)
then A21: - m < - n by XREAL_1:26;
- k < p - 1 by A20, SEQ_2:9;
then - m < p - 1 by A21, XXREAL_0:2;
then f . m < p - 1 by A17, XXREAL_0:2;
then (f . m) + 1 < p by XREAL_1:22;
then 1 < p - (f . m) by XREAL_1:22;
then r < abs (- ((f . m) - p)) by A19, ABSVALUE:def 1;
hence r < abs ((f . m) - p) by COMPLEX1:138; :: thesis: verum

end;

rng f c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in X )
assume x in rng f ; :: thesis: x in X
then consider y being set such that
A22: y in dom f and
A23: x = f . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A22, FUNCT_2:def 1;
f . y in X by A17;
hence x in X by A23; :: thesis: verum

end;

then ex s2 being Real_Sequence st
( s2 is subsequence of f & s2 is convergent & lim s2 in X ) by A1, Def3;
hence contradiction by A18, Th27; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum