let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: sin (angle (p1,p2,p3)) = - (sin (angle (p3,p2,p1)))

per cases ( angle (p1,p2,p3) = 0 or angle (p1,p2,p3) <> 0 ) ;

suppose A1: angle (p1,p2,p3) = 0 ; :: thesis: sin (angle (p1,p2,p3)) = - (sin (angle (p3,p2,p1)))

then angle (p3,p2,p1) = 0 by EUCLID_3:36;
hence sin (angle (p1,p2,p3)) = - (sin (angle (p3,p2,p1))) by A1, SIN_COS:31; :: thesis: verum

end;

suppose angle (p1,p2,p3) <> 0 ; :: thesis: sin (angle (p1,p2,p3)) = - (sin (angle (p3,p2,p1)))

then angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3)) by EUCLID_3:37;
then sin (angle (p1,p2,p3)) = sin ((- (angle (p3,p2,p1))) + (2 * PI))
.= sin (- (angle (p3,p2,p1))) by SIN_COS:79
.= - (sin (angle (p3,p2,p1))) by SIN_COS:31 ;
hence sin (angle (p1,p2,p3)) = - (sin (angle (p3,p2,p1))) ; :: thesis: verum

end;

end;