let r be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
r ** X is bounded_below
let X be non empty Subset of REAL; :: thesis: ( X is bounded_below & 0 <= r implies r ** X is bounded_below )
assume that
A1: X is bounded_below and
A2: 0 <= r ; :: thesis: r ** X is bounded_below
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 LowerBound of r ** X

proof

let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not y in r ** X or 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 ex x being Real st
( y = r * x & x in X ) ;
hence r * b <= y by A2, A4, XREAL_1:64; :: thesis: verum

end;

hence r ** X is bounded_below ; :: thesis: verum