theorem :: EUCLID10:27

for x, y, z being Real st (x - ((- (2 * PI)) + y)) + z = PI holds
(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2