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 S₁[ object ] means c₁ in X;
deffunc H₁( object ) -> object = c₁;
set Y = { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) } ;
A2: X c= { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) }

proof

let i be Integer; :: according to MEMBERED:def 11 :: thesis: ( not i in X or i in { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) } )
A3: i in INT by INT_1:def 2;
assume A4: S₁[i] ; :: thesis: i in { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) }
then A5: i <= sup Z by Th4;
inf Z <= i by A4, Th3;
hence i in { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) } by A3, A4, A5; :: thesis: verum

end;

{ H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) } is finite from XXREAL_2:sch 1();
hence X is finite by A2; :: thesis: verum

end;

end;