theorem Th7: :: COMPLEX2:7
for a, b being Real st a in ].(PI / 2),PI.[ & b in ].(PI / 2),PI.[ holds
( a < b iff sin a > sin b )