let l be Element of NAT ; :: thesis: UsedIntLoc (Goto l) = {}
Goto l = 0 .--> (goto l) by SCMFSA8A:def 2;
hence UsedIntLoc (Goto l) = UsedIntLoc (goto l) by Th7
.= {} by SF_MASTR:19 ;
:: thesis: verum