:: deftheorem defines % IDEAL_1:def 23 :
for R being non empty multMagma
for I, J being Subset of R holds I % J = { a where a is Element of R : a * J c= I } ;