let p1, p, q, p2 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:9
.= (((1 - r1) * p) `1 ) + ((r1 * q) `1 ) by TOPREAL3:9
.= p1 `1 by A1, TOPREAL3:7
.= (((1 - r2) * p) `1 ) + ((r2 * q) `1 ) by A2, A4, TOPREAL3:7
.= ((1 - r2) * (p `1 )) + ((r2 * q) `1 ) by TOPREAL3:9
.= ((1 * (p `1 )) - (r2 * (p `1 ))) + (r2 * (q `1 )) by TOPREAL3:9
.= (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 Th37; :: thesis: verum