let X be integer-membered non empty set ; :: thesis: ( X is bounded_above implies X is right_end )
assume X is bounded_above ; :: thesis: X is right_end
then reconsider Y = X as integer-membered non empty bounded_above set ;
set s = sup Y;
A1: [\(sup Y)/] <= sup Y by INT_1:def 6;
[\(sup Y)/] is UpperBound of X
proof
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= [\(sup Y)/] )
assume x in X ; :: thesis: x <= [\(sup Y)/]
hence x <= [\(sup Y)/] by Th4, INT_1:54; :: thesis: verum
end;
then sup Y <= [\(sup Y)/] by Def3;
then reconsider s = sup Y as Integer by A1, XXREAL_0:1;
assume A2: not sup X in X ; :: according to XXREAL_2:def 6 :: thesis: contradiction
s - 1 is UpperBound of X
proof
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= s - 1 )
assume A3: x in X ; :: thesis: x <= s - 1
then reconsider i = x as Integer ;
i <= s by A3, Th4;
then i < s by A2, A3, XXREAL_0:1;
hence x <= s - 1 by INT_1:52; :: thesis: verum
end;
then s - 1 >= s by Def3;
hence contradiction by XREAL_1:146; :: thesis: verum