for r being Real st 0 <= r & r <= PI / 2 & cos r = 1 / 2 holds
r = PI / 3