theorem Th31: :: SIN_COS6:31
for r being Real st 0 <= r & r < (3 / 2) * PI holds
sin r > - 1