theorem Th15: :: SF_MASTR:15

for l being Nat holds UsedIntLoc (goto l) = {}