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:31; :: thesis: verum

end;

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