theorem :: SINCOS10:24

cosec | ].0,(PI / 2).] is one-to-one by Th20, FCONT_3:8;