theorem Th2: :: JGRAPH_6:2

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