theorem Th25: :: MORPH_01:25

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