let T1, T2 be Order of (n -tuples_on NAT); :: thesis: ( ( for p, q being Element of n -tuples_on NAT holds

( [p,q] in T1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds

( [p,q] in T2 iff p <= q ) ) implies T1 = T2 )

assume that

A11: for p, q being Element of n -tuples_on NAT holds

( [p,q] in T1 iff p <= q ) and

A12: for p, q being Element of n -tuples_on NAT holds

( [p,q] in T2 iff p <= q ) ; :: thesis: T1 = T2

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in T1 or [x,y] in T2 ) & ( not [x,y] in T2 or [x,y] in T1 ) )

thus ( [x,y] in T1 implies [x,y] in T2 ) :: thesis: ( not [x,y] in T2 or [x,y] in T1 )

then consider p, q being object such that

A17: [x,y] = [p,q] and

A18: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2;

reconsider p = p, q = q as Element of n -tuples_on NAT by A18;

p <= q by A12, A16, A17;

hence [x,y] in T1 by A11, A17; :: thesis: verum

( [p,q] in T1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds

( [p,q] in T2 iff p <= q ) ) implies T1 = T2 )

assume that

A11: for p, q being Element of n -tuples_on NAT holds

( [p,q] in T1 iff p <= q ) and

A12: for p, q being Element of n -tuples_on NAT holds

( [p,q] in T2 iff p <= q ) ; :: thesis: T1 = T2

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in T1 or [x,y] in T2 ) & ( not [x,y] in T2 or [x,y] in T1 ) )

thus ( [x,y] in T1 implies [x,y] in T2 ) :: thesis: ( not [x,y] in T2 or [x,y] in T1 )

proof

assume A16:
[x,y] in T2
; :: thesis: [x,y] in T1
assume A13:
[x,y] in T1
; :: thesis: [x,y] in T2

then consider p, q being object such that

A14: [x,y] = [p,q] and

A15: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2;

reconsider p = p, q = q as Element of n -tuples_on NAT by A15;

p <= q by A11, A13, A14;

hence [x,y] in T2 by A12, A14; :: thesis: verum

end;then consider p, q being object such that

A14: [x,y] = [p,q] and

A15: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2;

reconsider p = p, q = q as Element of n -tuples_on NAT by A15;

p <= q by A11, A13, A14;

hence [x,y] in T2 by A12, A14; :: thesis: verum

then consider p, q being object such that

A17: [x,y] = [p,q] and

A18: ( p in n -tuples_on NAT & q in n -tuples_on NAT ) by RELSET_1:2;

reconsider p = p, q = q as Element of n -tuples_on NAT by A18;

p <= q by A12, A16, A17;

hence [x,y] in T1 by A11, A17; :: thesis: verum