let G be Group; :: thesis: for H being Subgroup of G holds
( H is normal iff for g being Element of G holds H |^ g is Subgroup of H )
let H be Subgroup of G; :: thesis: ( H is normal iff for g being Element of G holds H |^ g is Subgroup of H )

hereby :: thesis: ( ( for g being Element of G holds H |^ g is Subgroup of H ) implies H is normal )

assume A1: H is normal ; :: thesis: for g being Element of G holds H |^ g is Subgroup of H
thus for g being Element of G holds H |^ g is Subgroup of H :: thesis: verum

proof

let g be Element of G; :: thesis: H |^ g is Subgroup of H
the carrier of (H |^ g) c= the carrier of H

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in the carrier of (H |^ g) or o in the carrier of H )
assume o in the carrier of (H |^ g) ; :: thesis: o in the carrier of H
then o in H |^ g ;
then consider b being Element of G such that
A4: ( o = b |^ g & b in H ) by Th58;
b |^ g in H by A4, A1, ThN1;
hence o in the carrier of H by A4; :: thesis: verum

end;

hence H |^ g is Subgroup of H by GROUP_2:57; :: thesis: verum

end;

end;

assume B: for g being Element of G holds H |^ g is Subgroup of H ; :: thesis: H is normal

now :: thesis: for g, h being Element of G st h in H holds
h |^ g in H

let g, h be Element of G; :: thesis: ( h in H implies h |^ g in H )
H |^ g is Subgroup of H by B;
then B1: the carrier of (H |^ g) c= the carrier of H by GROUP_2:def 5;
assume h in H ; :: thesis: h |^ g in H
then h |^ g in H |^ g by Th58;
hence h |^ g in H by B1; :: thesis: verum

end;

hence H is normal by ThN1; :: thesis: verum