:: deftheorem defines bounded_below SEQ_2:def 2 :
for f being real-valued Function holds
( f is bounded_below iff ex r being Real st
for y being object st y in dom f holds
r < f . y );