theorem Th1: :: RADIX_4:1

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