let r be Real; :: thesis: ( - 1 < r & r < 1 implies ( PI / 4 < arccot r & arccot r < (3 / 4) * PI ) )
assume A1: ( - 1 < r & r < 1 ) ; :: thesis: ( PI / 4 < arccot r & arccot r < (3 / 4) * PI )
then ( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI ) by Th62;
then A2: ( ( PI / 4 < arccot r & arccot r < (3 / 4) * PI ) or PI / 4 = arccot r or arccot r = (3 / 4) * PI ) by XXREAL_0:1;
thus ( PI / 4 < arccot r & arccot r < (3 / 4) * PI ) by A1, A2, Th16, Th50; :: thesis: verum