[.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def 12;
then cosec | [.(PI / 4),(PI / 2).] is decreasing by Th20, RFUNCT_2:29;
hence (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] is decreasing ; :: thesis: verum