theorem :: RCOMP_3:40

for r, s being Real st r <= s holds
for A being Subset of (Closed-Interval-TSpace (r,s)) holds A is real-bounded Subset of REAL