theorem Th7: :: GROUP_2:7

for G being Group
for A being Subset of G holds
( A <> {} iff A " <> {} )