let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for k1, k2 being natural Number holds
( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 )
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for k1, k2 being natural Number holds
( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 )
let k1, k2 be natural Number ; :: thesis: ( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 )
A1: ( k1 is Element of NAT & k2 is Element of NAT ) by ORDINAL1:def 12;
consider f2 being sequence of NAT such that
A2: ( f2 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n,T ) ) ) and
A3: il. (T,k2) = f2 . k2 by Def4;
consider f1 being sequence of NAT such that
A4: f1 is bijective and
A5: for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n,T ) and
A6: il. (T,k1) = f1 . k1 by Def4;
f1 = f2 by A4, A5, A2, Th2;
hence ( il. (T,k1) <= il. (T,k2),T iff k1 <= k2 ) by A1, A5, A6, A3; :: thesis: verum