let A, B, C, D be Point of (TOP-REAL 2); :: thesis: ( |.(A - B).| = |.(A - C).| & B in LSeg (A,D) & C in LSeg (A,D) implies B = C )
assume that
A1: |.(A - B).| = |.(A - C).| and
A2: B in LSeg (A,D) and
A3: C in LSeg (A,D) ; :: thesis: B = C
consider lambda being Real such that
A4: 0 <= lambda and
lambda <= 1 and
A6: B = ((1 - lambda) * A) + (lambda * D) by A2, RLTOPSP1:76;
consider mu being Real such that
A7: 0 <= mu and
mu <= 1 and
A9: C = ((1 - mu) * A) + (mu * D) by A3, RLTOPSP1:76;
A10: ((1 - 0) * A) + (0 * D) = ((1 - 0) * A) + (0. (TOP-REAL 2)) by RLVECT_1:10
.= 1 * A by RLVECT_1:4
.= A by RLVECT_1:def 8 ;
reconsider x1 = A, x2 = D as Element of REAL 2 by EUCLID:22;
A11: ( A = ((1 - 0) * x1) + (0 * x2) & B = ((1 - lambda) * x1) + (lambda * x2) ) by A6, A10;
A12: |.(A - B).| = |.(B - A).| by EUCLID_6:43
.= |.((lambda - 0) * (D - A)).| by A11, Th1
.= |.lambda.| * |.(D - A).| by TOPRNS_1:7
.= lambda * |.(D - A).| by A4, ABSVALUE:def 1 ;
A13: ( A = ((1 - 0) * x1) + (0 * x2) & C = ((1 - mu) * x1) + (mu * x2) ) by A9, A10;
A14: |.(A - C).| = |.(C - A).| by EUCLID_6:43
.= |.((mu - 0) * (D - A)).| by A13, Th1
.= |.mu.| * |.(D - A).| by TOPRNS_1:7
.= mu * |.(D - A).| by A7, ABSVALUE:def 1 ;
per cases ( A = D or A <> D ) ;
suppose A = D ; :: thesis: B = C
then ( B in {A} & C in {A} ) by A2, A3, RLTOPSP1:70;
then ( B = A & C = A ) by TARSKI:def 1;
hence B = C ; :: thesis: verum
end;
suppose A <> D ; :: thesis: B = C
then |.(D - A).| <> 0 by EUCLID_6:42;
then lambda = mu by A14, A1, A12, XCMPLX_1:5;
hence B = C by A6, A9; :: thesis: verum
end;
end;