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