let r be Real; :: thesis: for p being Point of (TOP-REAL 2) holds
( p in Vertical_Line r iff p `1 = r )
let p be Point of (TOP-REAL 2); :: thesis: ( p in Vertical_Line r iff p `1 = r )

hereby :: thesis: ( p `1 = r implies p in Vertical_Line r )

assume p in Vertical_Line r ; :: thesis: p `1 = r
then ex q being Point of (TOP-REAL 2) st
( q = p & q `1 = r ) ;
hence p `1 = r ; :: thesis: verum

end;

assume p `1 = r ; :: thesis: p in Vertical_Line r
hence p in Vertical_Line r ; :: thesis: verum