let e be set ; :: thesis: for k being Nat st e in k -SD holds
e is Integer
let k be Nat; :: thesis: ( e in k -SD implies e is Integer )
assume e in k -SD ; :: thesis: e is Integer
then ex t being Element of INT st
( e = t & t <= (Radix k) - 1 & t >= (- (Radix k)) + 1 ) ;
hence e is Integer ; :: thesis: verum