let k be Nat; :: thesis: ( 2 <= k implies SD_Add_Carry ((Radix k) - 1) = 1 )
assume k >= 2 ; :: thesis: SD_Add_Carry ((Radix k) - 1) = 1
then Radix k >= 4 by Th3;
then (Radix k) - 1 >= 4 - 1 by XREAL_1:9;
then (Radix k) - 1 > 2 by XXREAL_0:2;
hence SD_Add_Carry ((Radix k) - 1) = 1 by RADIX_1:def 10; :: thesis: verum