theorem Th9: :: GROUP_2:9
for G being non empty multMagma
for A, B being Subset of G holds
( ( A <> {} & B <> {} ) iff A * B <> {} )