let p be Point of (TOP-REAL 2); :: thesis: p in Vertical_Line (p `1)
p in { q where q is Point of (TOP-REAL 2) : p `1 = q `1 } ;
hence p in Vertical_Line (p `1) by JORDAN6:def 6; :: thesis: verum