let X be real-membered set ; :: thesis: ( not X is empty & X is bounded_above implies ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) ) )
assume that
A1: not X is empty and
A2: X is bounded_above ; :: thesis: ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )
consider p1 being real number such that
A3: p1 is UpperBound of X by A2, XXREAL_2:def 10;
A4: for r being real number st r in X holds
r <= p1 by A3, XXREAL_2:def 1;
defpred S₁[ Real] means for r being real number st r in X holds
r <= $1;
consider Y being Subset of REAL such that
A5: for p being Real holds
( p in Y iff S₁[p] ) from SUBSET_1:sch 3();
( X is Subset of REAL & ( for r, p being real number st r in X & p in Y holds
r <= p ) ) by A5, MEMBERED:3;
then consider g1 being real number such that
A6: for r, p being real number st r in X & p in Y holds
( r <= g1 & g1 <= p ) by AXIOMS:1;
reconsider g1 = g1 as Real by XREAL_0:def 1;
take g = g1; :: thesis: ( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )
A7: ex r1 being real number st r1 in X by A1, MEMBERED:9;

A8: now

given s1 being real number such that A9: 0 < s1 and
A10: for r being real number st r in X holds
not g - s1 < r ; :: thesis: contradiction
g - s1 in Y by A5, A10;
then g <= g - s1 by A7, A6;
then g - (g - s1) <= (g - s1) - (g - s1) by XREAL_1:9;
hence contradiction by A9; :: thesis: verum

end;

p1 is Real by XREAL_0:def 1;
then p1 in Y by A4, A5;
hence ( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) ) by A6, A8; :: thesis: verum