theorem Th2: :: GROUP_2:2

for x being object
for G being Group
for A being Subset of G holds
( x in A " iff ex g being Element of G st
( x = g " & g in A ) ) ;