let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for k1, k2 being natural number holds
( il. T,k1 <= il. T,k2,T iff k1 <= k2 )
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of 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 13;
consider f2 being Function of NAT ,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 Def12;
consider f1 being Function of NAT ,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 Def12;
f1 = f2 by A4, A5, A2, Th17;
hence ( il. T,k1 <= il. T,k2,T iff k1 <= k2 ) by A1, A5, A6, A3; :: thesis: verum