theorem Th21: :: EUCLID13:26

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