let X be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for M being Subset of X holds (0. X) + M = M
let M be Subset of X; :: thesis: (0. X) + M = M
A1: (0. X) + M = { ((0. X) + u) where u is Point of X : u in M } by RUSUB_4:def 9;
thus (0. X) + M c= M :: according to XBOOLE_0:def 10 :: thesis: M c= (0. X) + M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (0. X) + M or x in M )
assume x in (0. X) + M ; :: thesis: x in M
then ex u being Point of X st
( x = (0. X) + u & u in M ) by A1;
hence x in M by RLVECT_1:10; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in M or x in (0. X) + M )
assume A2: x in M ; :: thesis: x in (0. X) + M
then reconsider x = x as Point of X ;
(0. X) + x = x by RLVECT_1:10;
hence x in (0. X) + M by A1, A2; :: thesis: verum