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

A8: now :: thesis: for s1 being Real holds
( not 0 < s1 or ex r being Real st
( r in X & g - s1 < r ) )

given s1 being Real such that A9: 0 < s1 and
A10: for r being Real st r in X holds
not g - s1 < r ; :: thesis: contradiction
reconsider gs1 = g - s1 as Element of REAL by XREAL_0:def 1;
gs1 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 in REAL by XREAL_0:def 1;
then p1 in Y by A4, A5;
hence ( ( for r being Real st r in X holds
r <= g ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g - s < r ) ) ) by A6, A8; :: thesis: verum