theorem Th6: :: SCMFSA7B:6

for a, b, c being Int-Location st a <> b holds
not b := c destroys a