let k be Nat; :: thesis: k -SD_Sub_S c= (k + 1) -SD_Sub_S

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub_S or e in (k + 1) -SD_Sub_S )

assume e in k -SD_Sub_S ; :: thesis: e in (k + 1) -SD_Sub_S

then consider g being Element of INT such that

A1: e = g and

A2: g >= - (Radix (k -' 1)) and

A3: g <= (Radix (k -' 1)) - 1 ;

k -' 1 <= k by NAT_D:44;

then A4: 2 to_power (k -' 1) <= 2 to_power k by PRE_FF:8;

then (Radix (k -' 1)) - 1 <= (Radix k) - 1 by XREAL_1:9;

then (Radix (k -' 1)) - 1 <= (Radix ((k + 1) -' 1)) - 1 by NAT_D:34;

then A5: g <= (Radix ((k + 1) -' 1)) - 1 by A3, XXREAL_0:2;

- (Radix (k -' 1)) >= - (Radix k) by A4, XREAL_1:24;

then - (Radix (k -' 1)) >= - (Radix ((k + 1) -' 1)) by NAT_D:34;

then g >= - (Radix ((k + 1) -' 1)) by A2, XXREAL_0:2;

hence e in (k + 1) -SD_Sub_S by A1, A5; :: thesis: verum

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub_S or e in (k + 1) -SD_Sub_S )

assume e in k -SD_Sub_S ; :: thesis: e in (k + 1) -SD_Sub_S

then consider g being Element of INT such that

A1: e = g and

A2: g >= - (Radix (k -' 1)) and

A3: g <= (Radix (k -' 1)) - 1 ;

k -' 1 <= k by NAT_D:44;

then A4: 2 to_power (k -' 1) <= 2 to_power k by PRE_FF:8;

then (Radix (k -' 1)) - 1 <= (Radix k) - 1 by XREAL_1:9;

then (Radix (k -' 1)) - 1 <= (Radix ((k + 1) -' 1)) - 1 by NAT_D:34;

then A5: g <= (Radix ((k + 1) -' 1)) - 1 by A3, XXREAL_0:2;

- (Radix (k -' 1)) >= - (Radix k) by A4, XREAL_1:24;

then - (Radix (k -' 1)) >= - (Radix ((k + 1) -' 1)) by NAT_D:34;

then g >= - (Radix ((k + 1) -' 1)) by A2, XXREAL_0:2;

hence e in (k + 1) -SD_Sub_S by A1, A5; :: thesis: verum