set h = cot | ].0,PI.[;
A1:
[.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[
by Lm9, Lm10, XXREAL_2:def 12;
then (cot | [.(PI / 4),((3 / 4) * PI).]) " =
((cot | ].0,PI.[) | [.(PI / 4),((3 / 4) * PI).]) "
by RELAT_1:74
.=
((cot | ].0,PI.[) ") | ((cot | ].0,PI.[) .: [.(PI / 4),((3 / 4) * PI).])
by RFUNCT_2:17
.=
((cot | ].0,PI.[) ") | (rng ((cot | ].0,PI.[) | [.(PI / 4),((3 / 4) * PI).]))
by RELAT_1:115
.=
((cot | ].0,PI.[) ") | [.(- 1),1.]
by A1, Th22, RELAT_1:74
;
hence
arccot | [.(- 1),1.] = (cot | [.(PI / 4),((3 / 4) * PI).]) "
; verum