:: deftheorem Def4 defines bounded_below SEQ_2:def 4 :
for seq being Real_Sequence holds
( seq is bounded_below iff ex r being Real st
for n being Nat holds r < seq . n );