theorem Th4: :: RADIX_6:4

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