theorem :: EUCLID10:2

for a being Real holds cos (PI - a) = - (cos a)