theorem :: SIN_COS5:15

for x being Real st cos x <> 0 & sin x <> 0 holds
( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 )