let I be Program of ; :: thesis: not intloc 0 in dom I
dom I c= NAT by RELAT_1:def 18;
hence not intloc 0 in dom I by SCMFSA_2:59; :: thesis: verum