let I be Program of SCMPDS ; :: thesis: for a being Int_position holds not a in dom (Initialized I)
let a be Int_position ; :: thesis: not a in dom (Initialized I)
assume a in dom (Initialized I) ; :: thesis: contradiction
then A1: a in (dom I) \/ {(IC SCMPDS )} by Th27;

per cases ( a in dom I or a in {(IC SCMPDS )} ) by A1, XBOOLE_0:def 3;

suppose A2: a in dom I ; :: thesis: contradiction

dom I c= NAT by RELAT_1:def 18;
then reconsider l = a as Instruction-Location of SCMPDS by A2, AMI_1:def 4;
l = a ;
hence contradiction by SCMPDS_2:53; :: thesis: verum

end;

suppose a in {(IC SCMPDS )} ; :: thesis: contradiction

then a = IC SCMPDS by TARSKI:def 1;
hence contradiction by SCMPDS_2:52; :: thesis: verum

end;

end;