theorem Th30: :: SIN_COS6:30
for r being Real st 0 <= r & r < PI / 2 holds
sin r < 1