let l be Element of NAT ; :: thesis: not l in dom (Initialize ((intloc 0) .--> 1))
assume l in dom (Initialize ((intloc 0) .--> 1)) ; :: thesis: contradiction
then ( l = intloc 0 or l = IC ) by Th1;
hence contradiction by COMPOS_1:3, SCMFSA_2:84; :: thesis: verum