:: deftheorem defines arctan SIN_COS9:def 1 :
arctan = (tan | ].(- (PI / 2)),(PI / 2).[) " ;