theorem Th3: :: SEQ_2:3

for seq being Real_Sequence holds
( seq is bounded iff ex r being Real st
( 0 < r & ( for n being Nat holds |.(seq . n).| < r ) ) )