let r be Real; :: thesis: tan ((2 * PI) - r) = - (tan r)
tan ((2 * PI) - r) = (- (sin r)) / (cos ((2 * PI) - r)) by EUCLID10:3
.= - ((sin r) / (cos ((2 * PI) - r)))
.= - (tan r) by EUCLID10:4 ;
hence tan ((2 * PI) - r) = - (tan r) ; :: thesis: verum