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