theorem Th25: :: AMI_WSTD:25

for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower