:: deftheorem Def3 defines bounded_above SEQ_2:def 3 :
for seq being Real_Sequence holds
( seq is bounded_above iff ex r being Real st
for n being Nat holds seq . n < r );