let r be Real; :: thesis: for X being non empty real-membered set st ( for s being Real st s in X holds
s >= r ) & ( for t being Real st ( for s being Real 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 st s in X holds
s >= r ) & ( for t being Real st ( for s being Real st s in X holds
s >= t ) holds
r >= t ) implies r = lower_bound X )
assume that
A1: for s being Real st s in X holds
s >= r and
A2: for t being Real st ( for s being Real st s in X holds
s >= t ) holds
r >= t ; :: thesis: r = lower_bound X
A3: for s being Real st 0 < s holds
ex t being Real st
( t in X & not t >= r + s ) by A2, XREAL_1:29;
X is bounded_below

proof

take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of X
let s be ExtReal; :: 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, Def2; :: thesis: verum