defpred S_{1}[ 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_{1}[x,y] )
from RELSET_1:sch 2();

A2: R is_transitive_in n -tuples_on NAT

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

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

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

A2: R is_transitive_in n -tuples_on NAT

proof

A5:
R is_reflexive_in n -tuples_on NAT
by A1;
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;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

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

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;
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;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

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