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 ) ;
suppose X is empty ; :: thesis: ( X is real-bounded implies X is finite )
hence ( X is real-bounded implies X is finite ) ; :: thesis: verum
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 S1[ object ] means c1 in X;
deffunc H1( object ) -> object = c1;
set Y = { H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] ) } ;
A2: X c= { H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] ) }
proof
let i be Integer; :: according to MEMBERED:def 11 :: thesis: ( not i in X or i in { H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] ) } )
A3: i in INT by INT_1:def 2;
assume A4: S1[i] ; :: thesis: i in { H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] ) }
then A5: i <= sup Z by Th4;
inf Z <= i by ;
hence i in { H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] ) } by A3, A4, A5; :: thesis: verum
end;
{ H1(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S1[i] ) } is finite from hence X is finite by A2; :: thesis: verum
end;
end;