theorem Th1: :: SINCOS10:1

[.0,(PI / 2).[ c= dom sec