theorem Th2: :: GROUP_1A:48

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