:: deftheorem defines (-) MORPH_01:def 1 :
for E being RealLinearSpace
for A, B being binary-image of E holds A (-) B = { z where z is Element of E : for b being Element of E st b in B holds
z - b in A } ;