for th being Real st th in [.0,1.] holds
( 0 < cos . th & cos . th >= 1 / 2 )