theorem Th8: :: MORPH_01:8

for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (-) B = { v where v is Element of E : v + ((- 1) * B) c= A }