theorem Th7: :: RADIX_6:7

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