theorem :: RADIX_6:2

for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin (m,m,k)) > 0