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