theorem Th5: :: SCMFSA9A:5

for l being Nat holds UsedILoc (Goto l) = {}