let G be Group; :: thesis: 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
let N be Subgroup of G; :: thesis: ( ( for x, y being Element of G st y in N holds
(x * y) * (x ") in N ) implies N is normal )
assume A1: for x, y being Element of G st y in N holds
(x * y) * (x ") in N ; :: thesis: N is normal
for x being Element of G holds x * N c= N * x

proof

let x be Element of G; :: thesis: x * N c= N * x
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x * N or z in N * x )
assume A2: z in x * N ; :: thesis: z in N * x
then reconsider z = z as Element of G ;
consider z1 being Element of G such that
A3: ( z = x * z1 & z1 in N ) by A2, GROUP_2:103;
A4: (x * z1) * (x ") in N by A1, A3;
((x * z1) * (x ")) * x = z by A3, GROUP_3:1;
hence z in N * x by A4, GROUP_2:104; :: thesis: verum

end;

hence N is normal by GROUP_3:118; :: thesis: verum