theorem ThB42: :: GROUP_1A:243

for x being set
for G being addGroup
for g being Element of G
for A being Subset of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )