for th being Real st th in ].0,(PI / 2).[ holds
cos th > 0 by Th79;