theorem Th2: :: SIN_COS5:2

for x being Real st sin x <> 0 holds
cos x = (sin x) * (cot x)