theorem ThB119: :: GROUP_1A:318

for G being addGroup
for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H + a c= a + H )