for G being Group
for N being normal Subgroup of G
for x being Element of G holds (x * N) * (x ") c= carr N