let k be Nat; :: thesis: ( k >= 2 implies SD_Add_Carry (Radix k) = 1 )
assume k >= 2 ; :: thesis: SD_Add_Carry (Radix k) = 1
then Radix k > 2 by RADIX_4:1;
hence SD_Add_Carry (Radix k) = 1 by RADIX_1:def 10; :: thesis: verum