for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (-) B = meet { (b + A) where b is Element of E : b in B }