:: deftheorem defines < POLYNOM3:def 1 :
for n being Nat
for p, q being Element of n -tuples_on NAT holds
( p < q iff ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) ) );