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_reflexive_in n -tuples_on NAT

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in n -tuples_on NAT or [x,x] in R )
assume x in n -tuples_on NAT ; :: thesis: [x,x] in R
then reconsider x1 = x as Element of n -tuples_on NAT ;
x1 <= x1 ;
hence [x,x] in R by A1; :: thesis: verum

end;

A3: R is_antisymmetric_in n -tuples_on NAT

proof

let x, y be set ; :: 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
A4: x in n -tuples_on NAT and
A5: y in n -tuples_on NAT and
A6: [x,y] in R and
A7: [y,x] in R ; :: thesis: x = y
reconsider x1 = x, y1 = y as Element of n -tuples_on NAT by A4, A5;
( x1 <= y1 & y1 <= x1 ) by A1, A6, A7;
then ( ( x1 < y1 or x1 = y1 ) & ( y1 < x1 or y1 = x1 ) ) by Def2;
hence x = y ; :: thesis: verum

end;

A8: R is_transitive_in n -tuples_on NAT

proof

let x, y, z be set ; :: 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
A9: x in n -tuples_on NAT and
A10: y in n -tuples_on NAT and
A11: z in n -tuples_on NAT and
A12: [x,y] in R and
A13: [y,z] in R ; :: thesis: [x,z] in R
reconsider x1 = x, y1 = y, z1 = z as Element of n -tuples_on NAT by A9, A10, A11;
( x1 <= y1 & y1 <= z1 ) by A1, A12, A13;
then x1 <= z1 by Th5;
hence [x,z] in R by A1; :: thesis: verum

end;

( dom R = n -tuples_on NAT & field R = n -tuples_on NAT ) by A2, ORDERS_1:98;
then reconsider R = R as Order of (n -tuples_on NAT ) by A2, A3, A8, PARTFUN1:def 4, 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