theorem Thm17: :: EUCLID10:25

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