theorem ThX7: :: GROUP_1A:53

for G being addGroup
for A being Subset of G holds
( A <> {} iff - A <> {} )