theorem Th12: :: EUCLID_6:12

for p1, p3, p4, p being Point of (TOP-REAL 2) st p in LSeg (p1,p3) & p in LSeg (p1,p4) & p3 <> p4 & p <> p1 & not p3 in LSeg (p1,p4) holds
p4 in LSeg (p1,p3)