let r be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds

r ** X is bounded_above

let X be non empty Subset of REAL; :: thesis: ( X is bounded_below & r <= 0 implies r ** X is bounded_above )

assume that

A1: X is bounded_below and

A2: r <= 0 ; :: thesis: r ** X is bounded_above

consider b being Real such that

A3: b is LowerBound of X by A1;

A4: for x being Real st x in X holds

b <= x by A3, XXREAL_2:def 2;

r * b is UpperBound of r ** X

r ** X is bounded_above

let X be non empty Subset of REAL; :: thesis: ( X is bounded_below & r <= 0 implies r ** X is bounded_above )

assume that

A1: X is bounded_below and

A2: r <= 0 ; :: thesis: r ** X is bounded_above

consider b being Real such that

A3: b is LowerBound of X by A1;

A4: for x being Real st x in X holds

b <= x by A3, XXREAL_2:def 2;

r * b is UpperBound of r ** X

proof

hence
r ** X is bounded_above
; :: thesis: verum
let y be ExtReal; :: 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

A5: y = r * x and

A6: x in X ;

b <= x by A4, A6;

hence y <= r * b by A2, A5, XREAL_1:65; :: thesis: verum

end;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

A5: y = r * x and

A6: x in X ;

b <= x by A4, A6;

hence y <= r * b by A2, A5, XREAL_1:65; :: thesis: verum