theorem ThB32: :: GROUP_1A:233
for G being addGroup
for A, B being Subset of G holds
( A * B <> {} iff ( A <> {} & B <> {} ) )