theorem :: EUCLID_3:59
for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
not inside_of_triangle (p1,p2,p3) is empty