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