:: deftheorem defines arcsec1 SINCOS10:def 1 :
arcsec1 = (sec | [.0,(PI / 2).[) " ;