:: deftheorem defines ` GROUP_11:def 1 :
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 c= A } ;