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

hereby :: thesis: ( ex f being IL-Function of NAT ,S st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ) ) implies S is standard )

assume S is standard ; :: thesis: ex f being IL-Function of NAT ,S st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ) )
then consider f being IL-Function of NAT ,S such that
A1: f is bijective and
A2: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) by Def10;
thus ex f being IL-Function of NAT ,S st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ) ) :: thesis: verum

proof

take f ; :: thesis: ( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ) )
thus f is bijective by A1; :: thesis: for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) )
thus for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) by A1, A2, Th18; :: thesis: verum

end;

end;

given f being IL-Function of NAT ,S such that A3: f is bijective and
A4: for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ; :: thesis: S is standard
take f ; :: according to AMISTD_1:def 10 :: thesis: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) )
thus f is bijective by A3; :: thesis: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n )
thus for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) by A3, A4, Th18; :: thesis: verum