theorem Thm16: :: EUCLID10:24

for x being Real holds (sin (- x)) ^2 = (sin x) ^2