let X be RealLinearSpace; :: thesis: for r being Real holds r * {(0. X)} = {(0. X)}
let r be Real; :: thesis: r * {(0. X)} = {(0. X)}
thus r * {(0. X)} c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= r * {(0. X)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * {(0. X)} or x in {(0. X)} )
assume A1: x in r * {(0. X)} ; :: thesis: x in {(0. X)}
then reconsider x = x as Point of X ;
consider v being Point of X such that
A2: x = r * v and
A3: v in {(0. X)} by A1;
v = 0. X by A3, TARSKI:def 1;
then r * v = 0. X ;
hence x in {(0. X)} by A2, TARSKI:def 1; :: thesis: verum

end;

0. X in {(0. X)} by TARSKI:def 1;
then r * (0. X) in r * {(0. X)} ;
then 0. X in r * {(0. X)} ;
hence {(0. X)} c= r * {(0. X)} by ZFMISC_1:31; :: thesis: verum