let a be Real; :: thesis: cos ((3 * PI) - a) = - (cos a)
cos ((3 * PI) - a) = cos ((2 * PI) + (PI - a))
.= cos (PI - a) by SIN_COS:79
.= - (cos a) by EUCLID10:2 ;
hence cos ((3 * PI) - a) = - (cos a) ; :: thesis: verum