let X be real-membered set ; :: thesis: ( not X is empty & X is bounded_below implies ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) ) )
assume that
A1: not X is empty and
A2: X is bounded_below ; :: thesis: ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )
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
p1 <= r by A2, Def2;
reconsider X = X as Subset of REAL by MEMBERED:3;
defpred S₁[ Real] means for r being real number st r in X holds
$1 <= r;
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();
p1 is Real by XREAL_0:def 1;
then A6: p1 in Y by A4, A5;
for p, r being real number st p in Y & r in X holds
p <= r by A5;
then consider g1 being real number such that
A7: for p, r being real number st p in Y & r in X holds
( p <= g1 & g1 <= r ) 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
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )

now

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

end;

hence ( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) ) by A6, A7; :: thesis: verum