theorem :: DIFF_2:69

for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1))