for k being Nat holds k -SD_Sub_S c= INT