theorem Th58: :: EUCLID_3:58

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