theorem Th3: :: AMI_WSTD:3

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for f being sequence of NAT st f is bijective holds
( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) iff 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 ) ) )