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

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 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]
n is not UpperBound of X by A3, XXREAL_2:def 10;
then consider t being ExtReal such that
A5: ( t in X & n < t ) by XXREAL_2:def 1;
take t ; :: thesis: ( t is set & t is Element of REAL & S₁[n,t] )
thus ( t is set & t is Element of REAL & S₁[n,t] ) by A5; :: thesis: verum

end;

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

A7: now :: thesis: for n being Nat holds
( f . n in X & n < f . n )

let n be Nat; :: thesis: ( f . n in X & n < f . n )
n in NAT by ORDINAL1:def 12;
then ex q being Real 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 st p in X holds
ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )

proof

let p be Real; :: thesis: ( p in X implies ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) ) )
assume p in X ; :: thesis: ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )
consider q being Real such that
A9: q = 1 ;
take r = q; :: thesis: ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )
consider k being Nat such that
A10: p + 1 < k by SEQ_4:3;
take n = k; :: thesis: ( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )
thus 0 < r by A9; :: thesis: for m being Nat st n < m holds
r < |.((f . m) - p).|
let m be Nat; :: thesis: ( n < m implies r < |.((f . m) - p).| )
assume n < m ; :: thesis: r < |.((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:20;
hence r < |.((f . m) - p).| by A9, ABSVALUE:def 1; :: thesis: verum

end;

rng f c= X

proof

let x be object ; :: 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 object such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def 3;
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;
hence contradiction by A8, Th9; :: 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 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]
- n is not LowerBound of X by A13, XXREAL_2:def 9;
then consider t being ExtReal such that
A15: ( t in X & t < - n ) by XXREAL_2:def 2;
take t ; :: thesis: ( t is set & t is Element of REAL & S₁[n,t] )
thus ( t is set & t is Element of REAL & S₁[n,t] ) by A15; :: thesis: verum

end;

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

A17: now :: thesis: for n being Nat holds
( f . n in X & f . n < - n )

let n be Nat; :: thesis: ( f . n in X & f . n < - n )
n in NAT by ORDINAL1:def 12;
then ex q being Real 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 st p in X holds
ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )

proof

let p be Real; :: thesis: ( p in X implies ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) ) )
assume p in X ; :: thesis: ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )
consider q being Real such that
A19: q = 1 ;
take r = q; :: thesis: ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )
consider k being Nat such that
A20: |.(p - 1).| < k by SEQ_4:3;
take n = k; :: thesis: ( 0 < r & ( for m being Nat st n < m holds
r < |.((f . m) - p).| ) )
thus 0 < r by A19; :: thesis: for m being Nat st n < m holds
r < |.((f . m) - p).|
let m be Nat; :: thesis: ( n < m implies r < |.((f . m) - p).| )
assume n < m ; :: thesis: r < |.((f . m) - p).|
then A21: - m < - n by XREAL_1:24;
- k < p - 1 by A20, SEQ_2:1;
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:20;
then 1 < p - (f . m) by XREAL_1:20;
then r < |.(- ((f . m) - p)).| by A19, ABSVALUE:def 1;
hence r < |.((f . m) - p).| by COMPLEX1:52; :: thesis: verum

end;

rng f c= X

proof

let x be object ; :: 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 object such that
A22: y in dom f and
A23: x = f . y by FUNCT_1:def 3;
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;
hence contradiction by A18, Th9; :: thesis: verum

end;

end;