let T1, T2 be Order of (n -tuples_on NAT); ( ( 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 )
; T1 = T2
let x, y be object ; RELAT_1:def 2 ( ( 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 )
( not [x,y] in T2 or [x,y] in T1 )proof
assume A13:
[x,y] in T1
;
[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;
verum
end;
assume A16:
[x,y] in T2
; [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; verum