:: deftheorem defines <= POLYNOM3:def 2 :
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q iff ( p < q or p = q ) );