theorem Th11: :: SIN_COS5:11

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