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 r1 being real number such that
A3: r1 in X by A1, MEMBERED:9;
consider p1 being real number such that
A4: for r being real number st r in X holds
r <= p1 by A2, Def1;
A5: X is Subset of REAL by MEMBERED:3;
defpred S₁[ Real] means for r being real number st r in X holds
r <= $1;
consider Y being Subset of REAL such that
A6: for p being Real holds
( p in Y iff S₁[p] ) from SUBSET_1:sch 3();
p1 is Real by XREAL_0:def 1;
then A7: p1 in Y by A4, A6;
for r, p being real number st r in X & p in Y holds
r <= p by A6;
then consider g1 being real number such that
A8: for r, p being real number st r in X & p in Y holds
( r <= g1 & g1 <= p ) by A5, AXIOMS:26;
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 ) ) )

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 A6, A10;
then g <= g - s1 by A3, A8;
then g - (g - s1) <= (g - s1) - (g - s1) by XREAL_1:11;
hence contradiction by A9; :: thesis: verum

end;

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 A7, A8; :: thesis: verum