theorem Th1: :: JGRAPH_7:1

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