theorem :: SEQ_4:4

for X being Subset of REAL holds
( X is real-bounded iff ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) )