for x being Real st sin x <> 0 holds
(cosec x) ^2 = 1 + ((cot x) ^2)