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