theorem Th49: :: JORDAN6:49

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 )

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 )