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