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

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