let r be Real; :: thesis: for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X }
let X be Subset of REAL ; :: thesis: r ** X = { (r * x) where x is Real : x in X }
thus r ** X c= { (r * x) where x is Real : x in X } :: according to XBOOLE_0:def 10 :: thesis: { (r * x) where x is Real : x in X } c= r ** X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in r ** X or y in { (r * x) where x is Real : x in X } )
assume y in r ** X ; :: thesis: y in { (r * x) where x is Real : x in X }
then ex z being Real st
( z in X & y = r * z ) by Def2;
hence y in { (r * x) where x is Real : x in X } ; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { (r * x) where x is Real : x in X } or y in r ** X )
assume y in { (r * x) where x is Real : x in X } ; :: thesis: y in r ** X
then ex z being Real st
( y = r * z & z in X ) ;
hence y in r ** X by Def2; :: thesis: verum