let r be Real; :: thesis: ( sin (r - PI) = - (sin r) & cos (r - PI) = - (cos r) )
thus sin (r - PI) = ((sin r) * (cos PI)) - ((cos r) * (sin PI)) by Th3
.= - (sin r) by SIN_COS:77 ; :: thesis: cos (r - PI) = - (cos r)
thus cos (r - PI) = ((cos r) * (cos PI)) + ((sin r) * (sin PI)) by Th3
.= - (cos r) by SIN_COS:77 ; :: thesis: verum