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;
[\(sup Y)/] is UpperBound of X

proof

let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= [\(sup Y)/] )
assume Z: x in X ; :: thesis: x <= [\(sup Y)/]
thus x <= [\(sup Y)/] by Z, Th3B, INT_1:81; :: thesis: verum

end;

then A: sup Y <= [\(sup Y)/] by Def3;
[\(sup Y)/] <= sup Y by INT_1:def 4;
then reconsider s = sup Y as Integer by A, XXREAL_0:1;
assume Z: not sup X in X ; :: according to XXREAL_2:def 6 :: thesis: contradiction
s - 1 is UpperBound of X

proof

let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= s - 1 )
assume ZZ: x in X ; :: thesis: x <= s - 1
then reconsider i = x as Integer ;
i <= s by ZZ, Th3B;
then i < s by Z, ZZ, XXREAL_0:1;
hence x <= s - 1 by INT_1:79; :: thesis: verum

end;

then s - 1 >= s by Def3;
hence contradiction by XREAL_1:148; :: thesis: verum