let G be Group; :: thesis: for N being normal Subgroup of G
for x being Element of G holds (x * N) * (x ") c= carr N
let N be normal Subgroup of G; :: thesis: for x being Element of G holds (x * N) * (x ") c= carr N
let x be Element of G; :: thesis: (x * N) * (x ") c= carr N
x * N c= N * x by GROUP_3:118;
then A1: (x * N) * (x ") c= (N * x) * (x ") by GROUP_3:5;
(N * x) * (x ") = N * (x * (x ")) by GROUP_2:107
.= N * (1_ G) by GROUP_1:def 5 ;
hence (x * N) * (x ") c= carr N by A1, GROUP_2:109; :: thesis: verum