for G being Group
for N, H being Subgroup of G
for x being Element of G st x * N c= carr H holds
x in N ` H ;