theorem Th6: :: EUCLID13:6

for r being Real holds tan ((2 * PI) - r) = - (tan r)