theorem :: GROUP_3:120

for G being Group
for H being Subgroup of G holds
( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )