let X be Subset of REAL; :: thesis: for r being Real st X <> {} & ( for r9 being Real st r9 in X holds
r <= r9 ) holds
lower_bound X >= r
let r be Real; :: thesis: ( X <> {} & ( for r9 being Real st r9 in X holds
r <= r9 ) implies lower_bound X >= r )
assume that
A1: X <> {} and
A2: for r9 being Real st r9 in X holds
r <= r9 ; :: thesis: lower_bound X >= r
for r9 being ext-real number st r9 in X holds
r <= r9 by A2;
then r is LowerBound of X by XXREAL_2:def 2;
then A3: X is bounded_below by XXREAL_2:def 9;

now

let r9 be real number ; :: thesis: ( r9 > 0 implies (lower_bound X) + r9 >= r )
assume r9 > 0 ; :: thesis: (lower_bound X) + r9 >= r
then consider r1 being real number such that
A4: r1 in X and
A5: r1 < (lower_bound X) + r9 by A1, A3, Def5;
r <= r1 by A2, A4;
hence (lower_bound X) + r9 >= r by A5, XXREAL_0:2; :: thesis: verum

end;

hence lower_bound X >= r by XREAL_1:43; :: thesis: verum