for G being Group
for N being Subgroup of G st ( for x, y being Element of G st y in N holds
(x * y) * (x ") in N ) holds
N is normal