let r be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
r ** X is bounded_below
let X be non empty Subset of REAL ; :: thesis: ( X is bounded_above & r <= 0 implies r ** X is bounded_below )
assume A1: ( X is bounded_above & r <= 0 ) ; :: thesis: r ** X is bounded_below
then consider b being real number such that
A2: for x being real number st x in X holds
x <= b by SEQ_4:def 1;
for y being real number st y in r ** X holds
r * b <= y

proof

let y be real number ; :: thesis: ( y in r ** X implies r * b <= y )
assume y in r ** X ; :: thesis: r * b <= y
then y in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A3: ( y = r * x & x in X ) ;
thus r * b <= y by A1, A2, A3, XREAL_1:67; :: thesis: verum

end;

hence r ** X is bounded_below by SEQ_4:def 2; :: thesis: verum