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 )

proof

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;

assume A16: [x,y] in T2 ; :: thesis: [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