let G be strict Group; :: thesis: for H being strict Subgroup of G holds
( H is normal Subgroup of G iff Normalizator H = G )
let H be strict Subgroup of G; :: thesis: ( H is normal Subgroup of G iff Normalizator H = G )
thus ( H is normal Subgroup of G implies Normalizator H = G ) :: thesis: ( Normalizator H = G implies H is normal Subgroup of G )

proof

assume A1: H is normal Subgroup of G ; :: thesis: Normalizator H = G

now

let a be Element of G; :: thesis: a in Normalizator H
H |^ a = H by A1, Def13;
hence a in Normalizator H by Th160; :: thesis: verum

end;

hence Normalizator H = G by GROUP_2:62; :: thesis: verum

end;

assume A2: Normalizator H = G ; :: thesis: H is normal Subgroup of G
H is normal

proof

let a be Element of G; :: according to GROUP_3:def 13 :: thesis: H |^ a = multMagma(# the carrier of H, the multF of H #)
a in Normalizator H by A2, STRUCT_0:def 5;
then ex b being Element of G st
( b = a & H |^ b = H ) by Th160;
hence H |^ a = multMagma(# the carrier of H, the multF of H #) ; :: thesis: verum

end;

hence H is normal Subgroup of G ; :: thesis: verum