let G be non empty addMagma ; :: thesis: for A being Subset of G holds
( ({} the carrier of G) + A = {} & A + ({} the carrier of G) = {} )
let A be Subset of G; :: thesis: ( ({} the carrier of G) + A = {} & A + ({} the carrier of G) = {} )

A1: now :: thesis: not A + ({} the carrier of G) <> {}

set x = the Element of A + ({} the carrier of G);
assume A + ({} the carrier of G) <> {} ; :: thesis: contradiction
then ex g1, g2 being Element of G st
( the Element of A + ({} the carrier of G) = g1 + g2 & g1 in A & g2 in {} the carrier of G ) by ThX8;
hence contradiction ; :: thesis: verum

end;

now :: thesis: not ({} the carrier of G) + A <> {}

set x = the Element of ({} the carrier of G) + A;
assume ({} the carrier of G) + A <> {} ; :: thesis: contradiction
then ex g1, g2 being Element of G st
( the Element of ({} the carrier of G) + A = g1 + g2 & g1 in {} the carrier of G & g2 in A ) by ThX8;
hence contradiction ; :: thesis: verum

end;

hence ( ({} the carrier of G) + A = {} & A + ({} the carrier of G) = {} ) by A1; :: thesis: verum