theorem Th119: :: GROUP_3:119

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