let r be real number ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 holds
LSeg p1,p2 meets Vertical_Line r
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 `1 <= r & r <= p2 `1 implies LSeg p1,p2 meets Vertical_Line r )
assume that
A1: p1 `1 <= r and
A2: r <= p2 `1 ; :: thesis: LSeg p1,p2 meets Vertical_Line r
set a = p1 `1 ;
set b = p2 `1 ;
set l = (r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ));
set k = ((1 - ((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * p1) + (((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2);
A3: (p1 `1 ) - (p1 `1 ) <= r - (p1 `1 ) by A1, XREAL_1:11;
A4: r - (p1 `1 ) <= (p2 `1 ) - (p1 `1 ) by A2, XREAL_1:11;
then (r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )) <= 1 by A3, XREAL_1:185;
then A5: ((1 - ((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * p1) + (((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) in LSeg p1,p2 by A3, A4;

per cases ( p1 `1 <> p2 `1 or p1 `1 = p2 `1 ) ;

suppose p1 `1 <> p2 `1 ; :: thesis: LSeg p1,p2 meets Vertical_Line r

then A6: (p2 `1 ) - (p1 `1 ) <> 0 ;
(((1 - ((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * p1) + (((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2)) `1 = ((1 - ((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `1 )) + (((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * (p2 `1 )) by TOPREAL9:41
.= (p1 `1 ) + (((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * ((p2 `1 ) - (p1 `1 )))
.= (p1 `1 ) + (r - (p1 `1 )) by A6, XCMPLX_1:88 ;
then ((1 - ((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * p1) + (((r - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) in Vertical_Line r by JORDAN6:34;
hence LSeg p1,p2 meets Vertical_Line r by A5, XBOOLE_0:3; :: thesis: verum

end;

suppose A7: p1 `1 = p2 `1 ; :: thesis: LSeg p1,p2 meets Vertical_Line r

A8: p1 in LSeg p1,p2 by RLTOPSP1:69;
p1 `1 = r by A1, A2, A7, XXREAL_0:1;
then p1 in Vertical_Line r by JORDAN6:34;
hence LSeg p1,p2 meets Vertical_Line r by A8, XBOOLE_0:3; :: thesis: verum

end;

end;