theorem Th9: :: AMI_WSTD:9

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 l1, l2 being Element of NAT holds
( locnum (l1,T) <= locnum (l2,T) iff l1 <= l2,T )