:: deftheorem Def2 defines lower_bound SEQ_4:def 2 :
for X being real-membered set st not X is empty & X is bounded_below holds
for b₂ being Real holds
( b₂ = lower_bound X iff ( ( for r being Real st r in X holds
b₂ <= r ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & r < b₂ + s ) ) ) );