[.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
then (cot | ].0 ,PI .[) | [.(PI / 4),((3 / 4) * PI ).] = cot | [.(PI / 4),((3 / 4) * PI ).] by RELAT_1:103;
hence cot | [.(PI / 4),((3 / 4) * PI ).] is one-to-one ; :: thesis: verum