for m, k being Nat
for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds
SDDec r > SDDec (M0 r)