[.(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:74;
hence cot | [.(PI / 4),((3 / 4) * PI).] is one-to-one ; :: thesis: verum