:: deftheorem defines ~ GROUP_11:def 2 :
for G being Group
for A being Subset of G
for N being Subgroup of G holds N ~ A = { x where x is Element of G : x * N meets A } ;