let X be non empty real-membered set ; :: thesis: for t being Real st ( for s being Real st s in X holds
s >= t ) holds
lower_bound X >= t
set r = lower_bound X;
let t be Real; :: thesis: ( ( for s being Real st s in X holds
s >= t ) implies lower_bound X >= t )
assume A1: for s being Real st s in X holds
s >= t ; :: thesis: lower_bound X >= t
set s = t - (lower_bound X);
assume lower_bound X < t ; :: thesis: contradiction
then A2: t - (lower_bound X) > 0 by XREAL_1:50;
X is bounded_below
proof
take t ; :: according to XXREAL_2:def 9 :: thesis: t is LowerBound of X
let s be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not s in X or t <= s )
thus ( not s in X or t <= s ) by A1; :: thesis: verum
end;
then ex t9 being Real st
( t9 in X & t9 < (lower_bound X) + (t - (lower_bound X)) ) by A2, Def2;
hence contradiction by A1; :: thesis: verum