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