theorem Th27: :: GROUP_2:27

for x being object
for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )