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 ;

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 )
;

end;

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;then ( B = A & C = A ) by TARSKI:def 1;

hence B = C ; :: thesis: verum

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;then lambda = mu by A14, A1, A12, XCMPLX_1:5;

hence B = C by A6, A9; :: thesis: verum