let r be Real; :: 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:9;
A4: r - (p1 `1) <= (p2 `1) - (p1 `1) by A2, XREAL_1:9;
then (r - (p1 `1)) / ((p2 `1) - (p1 `1)) <= 1 by A3, XREAL_1:183;
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:87 ;
then ((1 - ((r - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + (((r - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) in Vertical_Line r by JORDAN6:31;
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:68;
p1 `1 = r by A1, A2, A7, XXREAL_0:1;
then p1 in Vertical_Line r by JORDAN6:31;
hence LSeg (p1,p2) meets Vertical_Line r by A8, XBOOLE_0:3; :: thesis: verum

end;

end;