:: deftheorem defines standard AMISTD_1:def 6 :
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 standard iff for m, n being Nat holds
( m <= n iff ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) ) );