theorem Thm1: :: EUCLID10:1

for a being Real holds sin (PI - a) = sin a