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