let V be non empty Abelian right_zeroed addLoopStr ; :: thesis: for A being Subset of V holds (0. V) + A = A
let A be Subset of V; :: thesis: (0. V) + A = A
thus (0. V) + A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= (0. V) + A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (0. V) + A or x in A )
assume x in (0. V) + A ; :: thesis: x in A
then ex s being Element of V st
( x = (0. V) + s & s in A ) ;
hence x in A by RLVECT_1:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (0. V) + A )
assume A1: x in A ; :: thesis: x in (0. V) + A
then reconsider v = x as Element of V ;
(0. V) + v = v by RLVECT_1:def 4;
hence x in (0. V) + A by A1; :: thesis: verum