theorem Th103: :: GROUP_1A:149

for x being object
for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( x in a + H iff ex g being Element of G st
( x = a + g & g in H ) )