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