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