theorem ThA16: :: GROUP_1A:62

for G being non empty addMagma
for A being Subset of G holds
( ({} the carrier of G) + A = {} & A + ({} the carrier of G) = {} )