let A, B, C be Point of (TOP-REAL 2); ( not angle (A,B,C) is zero implies sin ((angle (C,B,A)) / 3) = (((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3))) )
assume
not angle (A,B,C) is zero
; sin ((angle (C,B,A)) / 3) = (((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3)))
then sin ((1 / 3) * (angle (C,B,A))) =
((sin ((2 * PI) / 3)) * (cos ((1 / 3) * (angle (A,B,C))))) - ((cos (((1 / 3) * 2) * PI)) * (sin ((1 / 3) * (angle (A,B,C)))))
by Thm26
.=
(((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3)))
by Thm14, Thm15
;
hence
sin ((angle (C,B,A)) / 3) = (((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3)))
; verum