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

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

given s1 being Real such that A9: 0 < s1 and
A10: for r being Real st r in X holds
not r < g + s1 ; :: thesis: contradiction
reconsider gs1 = g + s1 as Element of REAL by XREAL_0:def 1;
gs1 in Y by A6, A10;
then g + s1 <= g by A3, A7;
then (g + s1) - g <= g - g by XREAL_1:9;
hence contradiction by A9; :: thesis: verum

end;

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