let G be Group; :: thesis: for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) holds
H is normal
let H be Subgroup of G; :: thesis: ( ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) implies H is normal )
assume A1: for a, b being Element of G st b is Element of H holds
b |^ a in H ; :: thesis: H is normal

now :: thesis: for a being Element of G holds H * a c= a * H

let a be Element of G; :: thesis: H * a c= a * H
thus H * a c= a * H :: thesis: verum

proof

set A = carr H;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in H * a or q in a * H )
assume q in H * a ; :: thesis: q in a * H
then consider b being Element of G such that
A2: q = b * a and
A3: b in H by GROUP_2:104;
b is Element of H by A3, STRUCT_0:def 5;
then b |^ a in H by A1;
then b |^ a in carr H by STRUCT_0:def 5;
then a * (((a ") * b) * a) in a * (carr H) by GROUP_2:27;
then a * ((a ") * (b * a)) in a * (carr H) by GROUP_1:def 3;
then (a * (a ")) * (b * a) in a * (carr H) by GROUP_1:def 3;
then ((a * (a ")) * b) * a in a * (carr H) by GROUP_1:def 3;
then ((1_ G) * b) * a in a * (carr H) by GROUP_1:def 5;
hence q in a * H by A2, GROUP_1:def 4; :: thesis: verum

end;

end;

hence H is normal by GROUP_3:119; :: thesis: verum