let k be Nat; :: thesis: k -SD_Sub_S c= k -SD_Sub
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub_S or e in k -SD_Sub )
assume e in k -SD_Sub_S ; :: thesis: e in k -SD_Sub
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 ;
(Radix (k -' 1)) + 1 >= (Radix (k -' 1)) + 0 by XREAL_1:7;
then - (Radix (k -' 1)) >= - ((Radix (k -' 1)) + 1) by XREAL_1:24;
then A4: g >= (- (Radix (k -' 1))) - 1 by A2, XXREAL_0:2;
(Radix (k -' 1)) + 0 >= (Radix (k -' 1)) + (- 1) by XREAL_1:7;
then Radix (k -' 1) >= g by A3, XXREAL_0:2;
hence e in k -SD_Sub by A1, A4; :: thesis: verum