let G be addGroup; :: thesis: for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds a + H c= H + a )
let H be Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for a being Element of G holds a + H c= H + a )
thus ( H is normal Subgroup of G implies for a being Element of G holds a + H c= H + a ) by Th117; :: thesis: ( ( for a being Element of G holds a + H c= H + a ) implies H is normal Subgroup of G )
assume A1: for a being Element of G holds a + H c= H + a ; :: thesis: H is normal Subgroup of G

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
(- a) + H c= H + (- a) by A1;
then a + ((- a) + H) c= a + (H + (- a)) by Th4;
then (a + (- a)) + H c= a + (H + (- a)) by ThB105;
then (0_ G) + H c= a + (H + (- a)) by Def5;
then carr H c= a + (H + (- a)) by ThB109;
then carr H c= (a + H) + (- a) by ThB106;
then (carr H) + a c= ((a + H) + (- a)) + a by Th4;
then H + a c= (a + H) + ((- a) + a) by ThB34;
then H + a c= (a + H) + (0_ G) by Def5;
hence H + a c= a + H by Th37; :: thesis: verum

end;

then for a being Element of G holds a + H = H + a by A1;
hence H is normal Subgroup of G by Th117; :: thesis: verum