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