theorem Th4: :: AMI_WSTD:4

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds
( S is weakly_standard iff ex f being sequence of NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) )