for A, B, C being Point of (TOP-REAL 2) st not angle (A,B,C) is zero holds
sin ((angle (C,B,A)) / 3) = (((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3)))