theorem :: EUCLID13:27

for A, B, C being Point of (TOP-REAL 2) st angle (B,A,C) <> angle (C,B,A) holds
sin (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 0