theorem ThB95: :: GROUP_1A:141

for x being object
for G being addGroup
for A being Subset of G
for H being Subgroup of G holds
( x in H + A iff ex g1, g2 being Element of G st
( x = g1 + g2 & g1 in H & g2 in A ) )