let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( ( 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 that
A1:
( p1 `1 = p2 `1 or p1 `2 = p2 `2 )
and
A2:
q1 in LSeg p1,p2
and
A3:
q2 in LSeg p1,p2
; ( q1 `1 = q2 `1 or q1 `2 = q2 `2 )
consider r2 being Real such that
A4:
q2 = ((1 - r2) * p1) + (r2 * p2)
and
0 <= r2
and
r2 <= 1
by A3;
consider r1 being Real such that
A5:
q1 = ((1 - r1) * p1) + (r1 * p2)
and
0 <= r1
and
r1 <= 1
by A2;
q1 `1 = (((1 - r1) * p1) `1 ) + ((r1 * p2) `1 )
by A5, TOPREAL3:7;
then
q1 `1 = ((1 - r1) * (p1 `1 )) + ((r1 * p2) `1 )
by TOPREAL3:9;
then A6:
q1 `1 = ((1 - r1) * (p1 `1 )) + (r1 * (p2 `1 ))
by TOPREAL3:9;
q2 `1 = (((1 - r2) * p1) `1 ) + ((r2 * p2) `1 )
by A4, TOPREAL3:7;
then
q2 `1 = ((1 - r2) * (p1 `1 )) + ((r2 * p2) `1 )
by TOPREAL3:9;
then A7:
q2 `1 = ((1 - r2) * (p1 `1 )) + (r2 * (p2 `1 ))
by TOPREAL3:9;
q1 `2 = (((1 - r1) * p1) `2 ) + ((r1 * p2) `2 )
by A5, TOPREAL3:7;
then
q1 `2 = ((1 - r1) * (p1 `2 )) + ((r1 * p2) `2 )
by TOPREAL3:9;
then A8:
q1 `2 = ((1 - r1) * (p1 `2 )) + (r1 * (p2 `2 ))
by TOPREAL3:9;
q2 `2 = (((1 - r2) * p1) `2 ) + ((r2 * p2) `2 )
by A4, TOPREAL3:7;
then
q2 `2 = ((1 - r2) * (p1 `2 )) + ((r2 * p2) `2 )
by TOPREAL3:9;
then A9:
q2 `2 = ((1 - r2) * (p1 `2 )) + (r2 * (p2 `2 ))
by TOPREAL3:9;