let k be Nat; :: thesis: k -SD c= (k + 1) -SD
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD or e in (k + 1) -SD )
assume e in k -SD ; :: thesis: e in (k + 1) -SD
then consider g being Element of INT such that
A1: e = g and
A2: g <= (Radix k) - 1 and
A3: g >= (- (Radix k)) + 1 ;
k < k + 1 by NAT_1:13;
then A4: 2 to_power k < 2 to_power (k + 1) by POWER:39;
then - (Radix k) > - (Radix (k + 1)) by XREAL_1:24;
then (- (Radix k)) + 1 > (- (Radix (k + 1))) + 1 by XREAL_1:6;
then A5: g >= (- (Radix (k + 1))) + 1 by A3, XXREAL_0:2;
(Radix k) - 1 < (Radix (k + 1)) - 1 by A4, XREAL_1:9;
then g <= (Radix (k + 1)) - 1 by A2, XXREAL_0:2;
hence e in (k + 1) -SD by A1, A5; :: thesis: verum