let k be Nat; :: thesis: for e being set st e in k -SD_Sub holds

e is Integer

let e be set ; :: thesis: ( e in k -SD_Sub implies e is Integer )

assume e in k -SD_Sub ; :: thesis: e is Integer

then ex t being Element of INT st

( e = t & t >= (- (Radix (k -' 1))) - 1 & t <= Radix (k -' 1) ) ;

hence e is Integer ; :: thesis: verum

e is Integer

let e be set ; :: thesis: ( e in k -SD_Sub implies e is Integer )

assume e in k -SD_Sub ; :: thesis: e is Integer

then ex t being Element of INT st

( e = t & t >= (- (Radix (k -' 1))) - 1 & t <= Radix (k -' 1) ) ;

hence e is Integer ; :: thesis: verum