theorem Th67: :: SINCOS10:67
arccosec1 * (cosec | [.(- (PI / 2)),0.[) = id [.(- (PI / 2)),0.[ by Lm27, Th27, FUNCT_1:39;