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