let p, p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `1 <> p2 `1 & p1 `2 = p2 `2 implies LSeg (p,q) is horizontal )
assume p1 in LSeg (p,q) ; :: thesis: ( not p2 in LSeg (p,q) or not p1 `1 <> p2 `1 or not p1 `2 = p2 `2 or LSeg (p,q) is horizontal )
then consider r1 being Real such that
A1: p1 = ((1 - r1) * p) + (r1 * q) and
0 <= r1 and
r1 <= 1 ;
assume p2 in LSeg (p,q) ; :: thesis: ( not p1 `1 <> p2 `1 or not p1 `2 = p2 `2 or LSeg (p,q) is horizontal )
then consider r2 being Real such that
A2: p2 = ((1 - r2) * p) + (r2 * q) and
0 <= r2 and
r2 <= 1 ;
assume that
A3: p1 `1 <> p2 `1 and
A4: p1 `2 = p2 `2 ; :: thesis: LSeg (p,q) is horizontal
(p `2) - ((r1 * (p `2)) - (r1 * (q `2))) = ((1 - r1) * (p `2)) + (r1 * (q `2))
.= ((1 - r1) * (p `2)) + ((r1 * q) `2) by TOPREAL3:4
.= (((1 - r1) * p) `2) + ((r1 * q) `2) by TOPREAL3:4
.= p1 `2 by A1, TOPREAL3:2
.= (((1 - r2) * p) `2) + ((r2 * q) `2) by A2, A4, TOPREAL3:2
.= ((1 - r2) * (p `2)) + ((r2 * q) `2) by TOPREAL3:4
.= ((1 * (p `2)) - (r2 * (p `2))) + (r2 * (q `2)) by TOPREAL3:4
.= (p `2) - ((r2 * (p `2)) - (r2 * (q `2))) ;
then A5: (r1 - r2) * (p `2) = (r1 - r2) * (q `2) ;
r1 - r2 <> 0 by A1, A2, A3;
then p `2 = q `2 by A5, XCMPLX_1:5;
hence LSeg (p,q) is horizontal by Th15; :: thesis: verum