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