[.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
then cot | [.(PI / 4),((3 / 4) * PI ).] is decreasing by Th8, RFUNCT_2:61;
hence (cot | [.(PI / 4),((3 / 4) * PI ).]) | [.(PI / 4),((3 / 4) * PI ).] is decreasing ; :: thesis: verum