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

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

suppose X is empty ; :: thesis: ( X is bounded implies X is finite )

hence ( X is bounded implies X is finite ) ; :: thesis: verum

end;

suppose S: not X is empty ; :: thesis: ( X is 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 S;
deffunc H₁( set ) -> set = c₁;
defpred S₁[ set ] means c₁ in X;
set m = inf Z;
set n = sup Z;
set Y = { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) } ;
A: { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) } is finite from XXREAL_2:sch 1();
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] ) } )
F: i in INT by INT_1:def 2;
assume Z: S₁[i] ; :: thesis: i in { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) }
then ( inf Z <= i & i <= sup Z ) by Th3, Th3B;
hence i in { H₁(i) where i is Element of INT : ( inf Z <= i & i <= sup Z & S₁[i] ) } by Z, F; :: thesis: verum

end;

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

end;

end;