seq + (- x) is Cauchy ;
hence seq - x is Cauchy by BHSP_1:56; :: thesis: verum