:: deftheorem defines bounded SEQ_2:def 8 :
for f being real-valued Function holds
( f is bounded iff ( f is bounded_above & f is bounded_below ) );