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 weakly_standard iff ex f being Function of NAT,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) )
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: ( S is weakly_standard iff ex f being Function of NAT,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) )

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

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

end;

end;

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