let k be Nat; :: thesis: ( 2 <= k implies k -SD_Sub c= k -SD )

assume A1: 2 <= k ; :: thesis: k -SD_Sub c= k -SD

then 1 + 1 <= k ;

then 1 <= k -' 1 by NAT_D:55;

then A2: Radix (k -' 1) >= 2 by Lm4;

then Radix (k -' 1) >= 1 by XXREAL_0:2;

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

then A3: (Radix k) + (- (Radix (k -' 1))) <= (Radix k) + (- 1) by XREAL_1:7;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub or e in k -SD )

assume e in k -SD_Sub ; :: thesis: e in k -SD

then consider g being Element of INT such that

A4: e = g and

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

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

(Radix (k -' 1)) + (Radix (k -' 1)) >= (Radix (k -' 1)) + 2 by A2, XREAL_1:6;

then (Radix k) + 0 >= ((Radix (k -' 1)) + 1) + 1 by A1, Lm1, XXREAL_0:2;

then (Radix k) - 1 >= ((Radix (k -' 1)) + 1) - 0 by XREAL_1:21;

then - ((Radix (k -' 1)) + 1) >= - ((Radix k) - 1) by XREAL_1:24;

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

(Radix k) + 0 = (Radix (k -' 1)) + (Radix (k -' 1)) by A1, Lm1, XXREAL_0:2;

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

hence e in k -SD by A4, A7; :: thesis: verum

assume A1: 2 <= k ; :: thesis: k -SD_Sub c= k -SD

then 1 + 1 <= k ;

then 1 <= k -' 1 by NAT_D:55;

then A2: Radix (k -' 1) >= 2 by Lm4;

then Radix (k -' 1) >= 1 by XXREAL_0:2;

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

then A3: (Radix k) + (- (Radix (k -' 1))) <= (Radix k) + (- 1) by XREAL_1:7;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub or e in k -SD )

assume e in k -SD_Sub ; :: thesis: e in k -SD

then consider g being Element of INT such that

A4: e = g and

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

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

(Radix (k -' 1)) + (Radix (k -' 1)) >= (Radix (k -' 1)) + 2 by A2, XREAL_1:6;

then (Radix k) + 0 >= ((Radix (k -' 1)) + 1) + 1 by A1, Lm1, XXREAL_0:2;

then (Radix k) - 1 >= ((Radix (k -' 1)) + 1) - 0 by XREAL_1:21;

then - ((Radix (k -' 1)) + 1) >= - ((Radix k) - 1) by XREAL_1:24;

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

(Radix k) + 0 = (Radix (k -' 1)) + (Radix (k -' 1)) by A1, Lm1, XXREAL_0:2;

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

hence e in k -SD by A4, A7; :: thesis: verum