theorem :: EUCLID_3:55

for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in outside_of_triangle (p1,p2,p3) iff ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 ) )