:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :
for n being Element of NAT
for b₂ being Order of (n -tuples_on NAT) holds
( b₂ = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds
( [p,q] in b₂ iff p <= q ) );