:: deftheorem Def4 defines il. AMI_WSTD:def 4 :
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 k being natural Number
for b₄ being Element of NAT holds
( b₄ = il. (S,k) iff ex f being sequence of NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b₄ = f . k ) );