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