theorem :: SIN_COS5:18

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