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