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 Instruction-Location of A;
A1: ObjectKind l = the Instructions of A by AMI_1:def 14;
assume for o being Object of holds not ObjectKind o is trivial ; :: according to AMI_7:def 2 :: thesis: A is with_non_trivial_Instructions
hence not the Instructions of A is trivial by A1; :: according to AMI_7:def 1 :: thesis: verum