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 )

hence p in Vertical_Line r ; :: thesis: verum

( 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 `1 = r
; :: thesis: p in Vertical_Line rassume
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;then ex q being Point of (TOP-REAL 2) st

( q = p & q `1 = r ) ;

hence p `1 = r ; :: thesis: verum

hence p in Vertical_Line r ; :: thesis: verum