for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )