theorem Th11: :: POLYNOM3:11

for i, j, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> holds
( i < j iff k1 < k2 )