let a be Real; :: thesis: cos ((2 * PI) - a) = cos a
cos ((2 * PI) - a) = (1 * (cos a)) + (0 * (sin a)) by SIN_COS:77, SIN_COS:83
.= cos a ;
hence cos ((2 * PI) - a) = cos a ; :: thesis: verum