:: deftheorem defines ~ GROUP_11:def 4 :
for G being Group
for H, N being Subgroup of G holds N ~ H = { x where x is Element of G : x * N meets carr H } ;