[.(PI / 4),(PI / 2).] c= ].0 ,(PI / 2).] by Lm12, XXREAL_2:def 12;
then (cosec | ].0 ,(PI / 2).]) | [.(PI / 4),(PI / 2).] = cosec | [.(PI / 4),(PI / 2).] by RELAT_1:103;
hence cosec | [.(PI / 4),(PI / 2).] is one-to-one ; :: thesis: verum