let X be integer-membered set ; :: thesis: ( X is real-bounded implies X is finite )

per cases
( X is empty or not X is empty )
;

end;

suppose A1:
not X is empty
; :: thesis: ( X is real-bounded implies X is finite )

assume
( X is bounded_below & X is bounded_above )
; :: according to XXREAL_2:def 11 :: thesis: X is finite

then reconsider Z = X as integer-membered non empty bounded_below bounded_above set by A1;

set m = inf Z;

set n = sup Z;

defpred S_{1}[ object ] means c_{1} in X;

deffunc H_{1}( object ) -> object = c_{1};

set Y = { H_{1}(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S_{1}[i] ) } ;

A2: X c= { H_{1}(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S_{1}[i] ) }
_{1}(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S_{1}[i] ) } is finite
from XXREAL_2:sch 1();

hence X is finite by A2; :: thesis: verum

end;then reconsider Z = X as integer-membered non empty bounded_below bounded_above set by A1;

set m = inf Z;

set n = sup Z;

defpred S

deffunc H

set Y = { H

A2: X c= { H

proof

{ H
let i be Integer; :: according to MEMBERED:def 11 :: thesis: ( not i in X or i in { H_{1}(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S_{1}[i] ) } )

A3: i in INT by INT_1:def 2;

assume A4: S_{1}[i]
; :: thesis: i in { H_{1}(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S_{1}[i] ) }

then A5: i <= sup Z by Th4;

inf Z <= i by A4, Th3;

hence i in { H_{1}(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S_{1}[i] ) }
by A3, A4, A5; :: thesis: verum

end;A3: i in INT by INT_1:def 2;

assume A4: S

then A5: i <= sup Z by Th4;

inf Z <= i by A4, Th3;

hence i in { H

hence X is finite by A2; :: thesis: verum