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