theorem Th20: :: EUCLID_6:20

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