theorem Th7: :: POLYNOM3:7

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