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