let X be non empty real-membered set ; :: thesis: for t being real number st ( for s being real number st s in X holds
s >= t ) holds
lower_bound X >= t
set r = lower_bound X;
let t be real number ; :: thesis: ( ( for s being real number st s in X holds
s >= t ) implies lower_bound X >= t )
assume A1: for s being real number st s in X holds
s >= t ; :: thesis: lower_bound X >= t
then A2: X is bounded_below by Def2;
set s = t - (lower_bound X);
assume lower_bound X < t ; :: thesis: contradiction
then t - (lower_bound X) > 0 by XREAL_1:52;
then consider t' being real number such that
A3: ( t' in X & t' < (lower_bound X) + (t - (lower_bound X)) ) by A2, Def5;
thus contradiction by A1, A3; :: thesis: verum