theorem Th3: :: AMISTD_1:3

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 k being Nat holds
( k + 1 in SUCC (k,S) & ( for j being Nat st j in SUCC (k,S) holds
k <= j ) ) )