theorem :: SINCOS10:63

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