for k being Nat holds k -SD_Sub_S c= (k + 1) -SD_Sub_S