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

A7: now

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

end;

p1 is Real by XREAL_0:def 1;
then p1 in Y by A3, A4;
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 A5, A7; :: thesis: verum