theorem Th3: :: RADIX_6:3

for m, k being Nat st k >= 2 holds
for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) >= SDDec r