theorem :: DIFF_2:72

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