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