theorem Thm26: :: EUCLID10:40

for A, B, C being Point of (TOP-REAL 2)
for r being positive Real st not angle (A,B,C) is zero holds
sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C)))))