let r be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
r ** X is bounded_above
let X be non empty Subset of REAL ; :: thesis: ( X is bounded_above & 0 <= r implies r ** X is bounded_above )
assume that
A1: X is bounded_above and
A2: 0 <= r ; :: thesis: r ** X is bounded_above
consider b being real number such that
B3: b is UpperBound of X by A1, XXREAL_2:def 10;
A3: for x being real number st x in X holds
x <= b by B3, XXREAL_2:def 1;
r * b is UpperBound of r ** X

proof

let y be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not y in r ** X or y <= r * b )
assume y in r ** X ; :: thesis: y <= r * b
then y in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A4: y = r * x and
A5: x in X ;
x <= b by A3, A5;
hence y <= r * b by A2, A4, XREAL_1:66; :: thesis: verum

end;

hence r ** X is bounded_above by XXREAL_2:def 10; :: thesis: verum