theorem Th23: :: EUCLID_6:23

for p1, p2, p3 being Point of (TOP-REAL 2) st p1,p2,p3 are_mutually_distinct & angle (p1,p2,p3) <= PI holds
( angle (p2,p3,p1) <= PI & angle (p3,p1,p2) <= PI )