let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & q1 in LSeg p1,p2 & q2 in LSeg p1,p2 & not q1 `1 = q2 `1 implies q1 `2 = q2 `2 )
assume A1:
( ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & q1 in LSeg p1,p2 & q2 in LSeg p1,p2 )
; :: thesis: ( q1 `1 = q2 `1 or q1 `2 = q2 `2 )
then
q1 in { (((1 - r) * p1) + (r * p2)) where r is Real : ( 0 <= r & r <= 1 ) }
;
then consider r1 being Real such that
A2:
( q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r1 & r1 <= 1 )
;
q2 in { (((1 - r) * p1) + (r * p2)) where r is Real : ( 0 <= r & r <= 1 ) }
by A1;
then consider r2 being Real such that
A3:
( q2 = ((1 - r2) * p1) + (r2 * p2) & 0 <= r2 & r2 <= 1 )
;
q1 `1 = (((1 - r1) * p1) `1 ) + ((r1 * p2) `1 )
by A2, TOPREAL3:7;
then
q1 `1 = ((1 - r1) * (p1 `1 )) + ((r1 * p2) `1 )
by TOPREAL3:9;
then A4:
q1 `1 = ((1 - r1) * (p1 `1 )) + (r1 * (p2 `1 ))
by TOPREAL3:9;
q1 `2 = (((1 - r1) * p1) `2 ) + ((r1 * p2) `2 )
by A2, TOPREAL3:7;
then
q1 `2 = ((1 - r1) * (p1 `2 )) + ((r1 * p2) `2 )
by TOPREAL3:9;
then A5:
q1 `2 = ((1 - r1) * (p1 `2 )) + (r1 * (p2 `2 ))
by TOPREAL3:9;
q2 `1 = (((1 - r2) * p1) `1 ) + ((r2 * p2) `1 )
by A3, TOPREAL3:7;
then
q2 `1 = ((1 - r2) * (p1 `1 )) + ((r2 * p2) `1 )
by TOPREAL3:9;
then A6:
q2 `1 = ((1 - r2) * (p1 `1 )) + (r2 * (p2 `1 ))
by TOPREAL3:9;
q2 `2 = (((1 - r2) * p1) `2 ) + ((r2 * p2) `2 )
by A3, TOPREAL3:7;
then
q2 `2 = ((1 - r2) * (p1 `2 )) + ((r2 * p2) `2 )
by TOPREAL3:9;
then A7:
q2 `2 = ((1 - r2) * (p1 `2 )) + (r2 * (p2 `2 ))
by TOPREAL3:9;