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

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

hence contradiction by XREAL_1:146; :: thesis: verum

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

then
sup Y <= [\(sup Y)/]
by Def3;
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;assume x in X ; :: thesis: x <= [\(sup Y)/]

hence x <= [\(sup Y)/] by Th4, INT_1:54; :: thesis: verum

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

then
s - 1 >= s
by Def3;
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;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

hence contradiction by XREAL_1:146; :: thesis: verum