theorem Th35: :: JGRAPH_1:36

for N being Nat
for p, p1, p2 being Point of (TOP-REAL N) st p in LSeg (p1,p2) holds
( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| )