theorem :: MORPH_01:23

for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
C (-) B c= C (-) A