let r be real number ; :: thesis: for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X
let X be non empty real-membered set ; :: thesis: ( ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) implies r = lower_bound X )
assume that
A1: for s being real number st s in X holds
s >= r and
A2: for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ; :: thesis: r = lower_bound X

A3: now

let s be real number ; :: thesis: ( 0 < s implies ex t being real number st
( t in X & not t >= r + s ) )
assume A4: 0 < s ; :: thesis: ex t being real number st
( t in X & not t >= r + s )
assume for t being real number st t in X holds
t >= r + s ; :: thesis: contradiction
then r >= r + s by A2;
hence contradiction by A4, XREAL_1:29; :: thesis: verum

end;

X is bounded_below

proof

take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of X
let s be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not s in X or r <= s )
assume s in X ; :: thesis: r <= s
hence r <= s by A1; :: thesis: verum

end;

hence r = lower_bound X by A1, A3, Def5; :: thesis: verum