for r being Real st 0 <= r & r < PI holds
cos r > - 1