theorem ThX8: :: GROUP_1A:54

for x being object
for G being non empty addMagma
for A, B being Subset of G holds
( x in A + B iff ex g, h being Element of G st
( x = g + h & g in A & h in B ) ) ;