let r, s be Real; :: thesis: ( r <= s implies for A being Subset of (Closed-Interval-TSpace (r,s)) holds A is real-bounded Subset of REAL )
assume r <= s ; :: thesis: for A being Subset of (Closed-Interval-TSpace (r,s)) holds A is real-bounded Subset of REAL
then A1: the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] by TOPMETR:18;
let A be Subset of (Closed-Interval-TSpace (r,s)); :: thesis: A is real-bounded Subset of REAL
( A is bounded_above & A is bounded_below ) by A1, XXREAL_2:43, XXREAL_2:44;
hence A is real-bounded Subset of REAL by A1, XBOOLE_1:1; :: thesis: verum