defpred S₁[ Element of n -tuples_on NAT, Element of n -tuples_on NAT] means $1 <= $2;
consider R being Relation of (n -tuples_on NAT),(n -tuples_on NAT) such that
A1: for x, y being Element of n -tuples_on NAT holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
A2: R is_transitive_in n -tuples_on NAT

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in n -tuples_on NAT or not y in n -tuples_on NAT or not z in n -tuples_on NAT or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A3: ( x in n -tuples_on NAT & y in n -tuples_on NAT & z in n -tuples_on NAT ) and
A4: ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
reconsider x1 = x, y1 = y, z1 = z as Element of n -tuples_on NAT by A3;
( x1 <= y1 & y1 <= z1 ) by A1, A4;
then x1 <= z1 by Th5;
hence [x,z] in R by A1; :: thesis: verum

end;

A5: R is_reflexive_in n -tuples_on NAT by A1;
then A6: ( dom R = n -tuples_on NAT & field R = n -tuples_on NAT ) by ORDERS_1:13;
R is_antisymmetric_in n -tuples_on NAT

proof

let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in n -tuples_on NAT or not y in n -tuples_on NAT or not [x,y] in R or not [y,x] in R or x = y )
assume that
A7: ( x in n -tuples_on NAT & y in n -tuples_on NAT ) and
A8: [x,y] in R and
A9: [y,x] in R ; :: thesis: x = y
reconsider x1 = x, y1 = y as Element of n -tuples_on NAT by A7;
x1 <= y1 by A1, A8;
then A10: ( x1 < y1 or x1 = y1 ) ;
y1 <= x1 by A1, A9;
hence x = y by A10; :: thesis: verum

end;

then reconsider R = R as Order of (n -tuples_on NAT) by A5, A2, A6, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take R ; :: thesis: for p, q being Element of n -tuples_on NAT holds
( [p,q] in R iff p <= q )
thus for p, q being Element of n -tuples_on NAT holds
( [p,q] in R iff p <= q ) by A1; :: thesis: verum