assume the Instruction-Counter of SCMPDS in NAT ; :: according to AMI_1:def 21 :: thesis: contradiction
hence contradiction by Th6; :: thesis: verum