for G being Group
for A being non empty Subset of G
for N being Subgroup of G holds N ~ (N ` (N ~ A)) = N ~ A