:: deftheorem defines + IDEAL_1:def 19 :
for R being addMagma
for I, J being Subset of R holds I + J = { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;