let r be Real; :: thesis: ( - 1 < r & r < 1 implies ( PI / 4 < arccot r & arccot r < (3 / 4) * PI ) )
assume that
A1: - 1 < r and
A2: r < 1 ; :: thesis: ( PI / 4 < arccot r & arccot r < (3 / 4) * PI )
A3: arccot r <= (3 / 4) * PI by A1, A2, Th64;
PI / 4 <= arccot r by A1, A2, Th64;
then ( ( PI / 4 < arccot r & arccot r < (3 / 4) * PI ) or PI / 4 = arccot r or arccot r = (3 / 4) * PI ) by A3, XXREAL_0:1;
hence ( PI / 4 < arccot r & arccot r < (3 / 4) * PI ) by A1, A2, Th18, Th52; :: thesis: verum