theorem Th16: :: GROUP_2:16

for G being non empty multMagma
for A being Subset of G holds
( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )