theorem Th1: :: SIN_COS5:1

for x being Real st cos x <> 0 holds
cosec x = (sec x) / (tan x)