theorem Th20: :: SIN_COS9:20

for x being set st x in [.(PI / 4),((3 / 4) * PI).] holds
cot . x in [.(- 1),1.]