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