for k being Nat st 2 <= k holds
2 < Radix k