theorem Th11: :: EUCLID11:16

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