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:45;
hence sin (angle p1,p2,p3) = - (sin (angle p3,p2,p1)) by A1, SIN_COS:34; :: 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:46;
then sin (angle p1,p2,p3) = sin ((- (angle p3,p2,p1)) + (2 * PI ))
.= sin (- (angle p3,p2,p1)) by SIN_COS:84
.= - (sin (angle p3,p2,p1)) by SIN_COS:34 ;
hence sin (angle p1,p2,p3) = - (sin (angle p3,p2,p1)) ; :: thesis: verum

end;

end;