theorem Th9: :: GROUP_1A:55
for G being non empty addMagma
for A, B being Subset of G holds
( ( A <> {} & B <> {} ) iff A + B <> {} )