:: deftheorem defines bounded TOPRNS_1:def 7 :
for N being Nat
for IT being Real_Sequence of N holds
( IT is bounded iff ex r being Real st
for n being Nat holds |.(IT . n).| < r );