theorem Th8: :: JORDAN1A:8

for p being Point of (TOP-REAL 2) holds p in Vertical_Line (p `1)