theorem :: MORPH_01:6

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 }