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