theorem Th1: :: SF_MASTR:1

for a1, a2, b1, b2 being Int-Location st a1 := b1 = a2 := b2 holds
( a1 = a2 & b1 = b2 )