theorem :: SINCOS10:22

sec | ].(PI / 2),PI.] is one-to-one by Th18, FCONT_3:8;