theorem :: EUCLID10:28

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