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