let l be Instruction-Location of SCM+FSA ; :: thesis: UsedIntLoc (goto l) = {}
A1: InsCode (goto l) = 6 by SCMFSA_2:47;
not 6 in {1,2,3,4,5} by ENUMSET1:def 3;
hence UsedIntLoc (goto l) = {} by A1, Def1; :: thesis: verum