:: deftheorem Def5 defines locnum AMI_WSTD:def 5 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l, b₄ being Nat holds
( b₄ = locnum (l,S) iff il. (S,b₄) = l );