let k be Nat; :: thesis: ( k >= 2 implies (Radix k) - 1 in k -SD )
assume A1: k >= 2 ; :: thesis: (Radix k) - 1 in k -SD
A2: k -SD = { w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 ) } by RADIX_1:def 2;
Radix k > 2 by A1, RADIX_4:1;
then Radix k > 1 by XXREAL_0:2;
then (Radix k) + (Radix k) > 1 + 1 by XREAL_1:10;
then A3: (Radix k) - 1 > (0 + 1) - (Radix k) by XREAL_1:23;
(Radix k) - 1 is Element of INT by INT_1:def 2;
hence (Radix k) - 1 in k -SD by A2, A3; :: thesis: verum