let p1, p2, p3 be Point of (TOP-REAL 2); sin (angle (p1,p2,p3)) = - (sin (angle (p3,p2,p1)))
per cases
( angle (p1,p2,p3) = 0 or angle (p1,p2,p3) <> 0 )
;
suppose
angle (
p1,
p2,
p3)
<> 0
;
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)))
;
verum end; end;