theorem Th7: :: SF_MASTR:7

for a1, a2 being Int-Location
for l1, l2 being Nat st a1 =0_goto l1 = a2 =0_goto l2 holds
( a1 = a2 & l1 = l2 )