[.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
hence dom (cot | [.(PI / 4),((3 / 4) * PI ).]) = [.(PI / 4),((3 / 4) * PI ).] by Th2, RELAT_1:91, XBOOLE_1:1; :: thesis: verum