let A be non empty stored-program definite AMI-Struct of N; ( A is with_non_trivial_ObjectKinds implies A is with_non_trivial_Instructions )
set l = the Element of NAT ;
A1:
the Object-Kind of A . the Element of NAT = the Instructions of A
by COMPOS_1:def 8;
assume A2:
for o being Object of A holds not ObjectKind o is trivial
; AMISTD_4:def 2 A is with_non_trivial_Instructions
A3:
the Element of NAT in NAT
;
NAT c= the carrier of A
by COMPOS_1:def 2;
then reconsider l = the Element of NAT as Object of A by A3;
ObjectKind l = the Instructions of A
by A1;
hence
not the Instructions of A is trivial
by A2; AMISTD_4:def 1 verum