theorem Th3: :: SFMASTR3:4

for aa, bb, cc being Int-Location st aa <> bb holds
not cc := bb refers aa