theorem Th7: :: AMISTD_4:7

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Out_U_Inp I