theorem Th1: :: JGRAPH_6:1

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