theorem Th3: :: JGRAPH_6:3

for a, b, d being Real
for p being Point of (TOP-REAL 2) st a <= b & p in LSeg (|[a,d]|,|[b,d]|) holds
( p `2 = d & a <= p `1 & p `1 <= b )