theorem Th69: :: SIN_COS:70

( [.0,1.] c= dom tan & ].0,1.[ c= dom tan )