theorem Th69: :: EUCLID13:85

for r, s, t, d being Real st (sin (2 * s)) * (cos d) = cos (2 * t) holds
(((r * (cos s)) ^2) + ((r * (sin s)) ^2)) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) = (2 * (r ^2)) * ((sin t) ^2)