for r being Real st - 1 <= r & r <= 1 & arccot r = PI / 2 holds
r = 0 by Th42, Th52;