X: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
set h = cot | ].0 ,PI .[;
(cot | [.(PI / 4),((3 / 4) * PI ).]) " = ((cot | ].0 ,PI .[) | [.(PI / 4),((3 / 4) * PI ).]) " by X, RELAT_1:103
.= ((cot | ].0 ,PI .[) " ) | ((cot | ].0 ,PI .[) .: [.(PI / 4),((3 / 4) * PI ).]) by RFUNCT_2:40
.= ((cot | ].0 ,PI .[) " ) | (rng ((cot | ].0 ,PI .[) | [.(PI / 4),((3 / 4) * PI ).])) by RELAT_1:148
.= ((cot | ].0 ,PI .[) " ) | [.(- 1),1.] by Th20, X, RELAT_1:103 ;
hence arccot | [.(- 1),1.] = (cot | [.(PI / 4),((3 / 4) * PI ).]) " ; :: thesis: verum