theorem Th7: :: SCMFSA7B:7

for a, b, c being Int-Location st a <> b holds
not AddTo (b,c) destroys a