theorem :: JORDAN1A:13

for p, q being Point of (TOP-REAL 2)
for s being Real st p in Vertical_Line s & q in Vertical_Line s holds
LSeg (p,q) c= Vertical_Line s