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:2;
then
q1 `1 = ((1 - r1) * (p1 `1)) + ((r1 * p2) `1)
by TOPREAL3:4;
then A6:
q1 `1 = ((1 - r1) * (p1 `1)) + (r1 * (p2 `1))
by TOPREAL3:4;
q2 `1 = (((1 - r2) * p1) `1) + ((r2 * p2) `1)
by A4, TOPREAL3:2;
then
q2 `1 = ((1 - r2) * (p1 `1)) + ((r2 * p2) `1)
by TOPREAL3:4;
then A7:
q2 `1 = ((1 - r2) * (p1 `1)) + (r2 * (p2 `1))
by TOPREAL3:4;
q1 `2 = (((1 - r1) * p1) `2) + ((r1 * p2) `2)
by A5, TOPREAL3:2;
then
q1 `2 = ((1 - r1) * (p1 `2)) + ((r1 * p2) `2)
by TOPREAL3:4;
then A8:
q1 `2 = ((1 - r1) * (p1 `2)) + (r1 * (p2 `2))
by TOPREAL3:4;
q2 `2 = (((1 - r2) * p1) `2) + ((r2 * p2) `2)
by A4, TOPREAL3:2;
then
q2 `2 = ((1 - r2) * (p1 `2)) + ((r2 * p2) `2)
by TOPREAL3:4;
then A9:
q2 `2 = ((1 - r2) * (p1 `2)) + (r2 * (p2 `2))
by TOPREAL3:4;