theorem Th8: :: AMI_WSTD:8

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 k1, k2 being natural Number holds
( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 )