for P1 being Subset of (TOP-REAL 2)
for r being Real
for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )