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

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

suppose p1 `2 <> p2 `2 ; :: thesis: LSeg p1,p2 meets Horizontal_Line r

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

end;

suppose A7: p1 `2 = p2 `2 ; :: thesis: LSeg p1,p2 meets Horizontal_Line r

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

end;

end;