theorem Th8: :: SIN_COS5:8

for x being Real st cos x <> 0 holds
cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2))