theorem Thm2: :: EUCLID10:5

for a being Real holds sin ((- (2 * PI)) + a) = sin a