let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds
( S is standard iff for k being Element of NAT holds
( k + 1 in SUCC k,S & ( for j being Element of NAT st j in SUCC k,S holds
k <= j ) ) )
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: ( S is standard iff for k being Element of NAT holds
( k + 1 in SUCC k,S & ( for j being Element of NAT st j in SUCC k,S holds
k <= j ) ) )

hereby :: thesis: ( ( for k being Element of NAT holds
( k + 1 in SUCC k,S & ( for j being Element of NAT st j in SUCC k,S holds
k <= j ) ) ) implies S is standard )

assume S is standard ; :: thesis: for k being Element of NAT holds
( k + 1 in SUCC k,S & ( for j being Element of NAT st j in SUCC k,S holds
k <= j ) )
hence for k being Element of NAT holds
( k + 1 in SUCC k,S & ( for j being Element of NAT st j in SUCC k,S holds
k <= j ) ) by Th18; :: thesis: verum

end;

assume A4: for k being Element of NAT holds
( k + 1 in SUCC k,S & ( for j being Element of NAT st j in SUCC k,S holds
k <= j ) ) ; :: thesis: S is standard
thus S is standard by A4, Th18; :: thesis: verum