theorem Th5: :: POLYNOM3:5

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