assume A1: the Instruction-Counter of (Trivial-AMI N) in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
the Instruction-Counter of (Trivial-AMI N) = NAT by Def2;
hence contradiction by A1; :: thesis: verum