theorem Th13: :: SIN_COS5:13

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