for G being Group
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 )