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 consider t being Element of INT such that
A1: e = t and
( t >= (- (Radix (k -' 1))) - 1 & t <= Radix (k -' 1) ) ;
thus e is Integer by A1; :: thesis: verum