defpred S1[ 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 S1[x,y] )
from RELSET_1:sch 2();
A2:
R is_transitive_in n -tuples_on NAT
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( 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 )
;
[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;
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
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
; 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; verum