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