let I be Instruction of (Trivial-AMI IL,N); :: according to AMISTD_2:def 20 :: thesis: I is Exec-preserving
thus I is Exec-preserving by Th46, AMISTD_1:56; :: thesis: verum