theorem :: GROUP_1A:81

for G being non empty addMagma
for a being Element of G holds
( ({} the carrier of G) + a = {} & a + ({} the carrier of G) = {} ) by ThA16;