let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds
( S is weakly_standard iff ex f being sequence of 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 with_non-empty_values IC-Ins-separated AMI-Struct over N; ( S is weakly_standard iff ex f being sequence of 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 ) ) ) ) )
given f being sequence of 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 ) )
; S is weakly_standard
take
f
; AMI_WSTD:def 3 ( 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; 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, Th3; verum