:: deftheorem defines <= AMI_WSTD:def 1 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Nat holds
( l1 <= l2,S iff ex f being non empty FinSequence of NAT st
( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) );