:: deftheorem defines (-) MATHMORP:def 3 :
for T being non empty addMagma
for X, B being Subset of T holds X (-) B = { y where y is Point of T : B + y c= X } ;