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 ExtReal 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 ;
now :: thesis: for r9 being Real st r9 > 0 holds
(lower_bound X) + r9 >= r
let r9 be Real; :: thesis: ( r9 > 0 implies (lower_bound X) + r9 >= r )
assume r9 > 0 ; :: thesis: (lower_bound X) + r9 >= r
then consider r1 being Real such that
A4: r1 in X and
A5: r1 < (lower_bound X) + r9 by A1, A3, Def2;
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:41; :: thesis: verum