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