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