theorem Th16: :: JGRAPH_1:16

for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds
( for x being set holds
( not x <> p2 or not x in (LSeg (p1,p2)) /\ (LSeg (p2,p3)) ) or p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) )