let A, B, C be Point of (TOP-REAL 2); :: thesis: ( C in Line (A,B) & |.(A - C).| = |.(B - C).| implies C in LSeg (A,B) )
assume that
A1: C in Line (A,B) and
A2: |.(A - C).| = |.(B - C).| ; :: thesis: C in LSeg (A,B)

per cases ( A = B or A <> B ) ;

suppose A3: A = B ; :: thesis: C in LSeg (A,B)

reconsider rA = A, rB = B as Element of REAL 2 by EUCLID:22;
( Line (rA,rA) = Line (A,A) & Line (rA,rB) = Line (A,B) ) by Th4;
then Line (A,B) = {A} by A3, Th3;
hence C in LSeg (A,B) by A1, A3, RLTOPSP1:70; :: thesis: verum

end;

suppose A <> B ; :: thesis: C in LSeg (A,B)

then A4: |.(A - B).| <> 0 by EUCLID_6:42;
reconsider rA = A, rB = B, rC = C as Element of REAL 2 by EUCLID:22;
C in Line (rA,rB) by A1, Th4;
then consider a being Real such that
A5: C = ((1 - a) * rA) + (a * rB) ;
set n = 2;
rA - rC = rA - (((1 * rA) + ((- a) * rA)) + (a * rB)) by A5, EUCLIDLP:11
.= rA + ((((- 1) * rA) + ((- (- a)) * rA)) + ((- a) * rB)) by EUCLIDLP:14
.= rA + (((- 1) * rA) + ((a * rA) + ((- a) * rB))) by RVSUM_1:15
.= (rA - rA) + ((a * rA) + ((- a) * rB)) by RVSUM_1:15
.= (0* 2) + ((a * rA) + ((- a) * rB)) by EUCLIDLP:2
.= (a * rA) + ((- a) * rB) by EUCLID_4:1
.= a * (rA - rB) by EUCLIDLP:12 ;
then A6: |.(A - C).| = |.a.| * |.(A - B).| by EUCLID:11;
rB - rC = (rB - (a * rB)) - ((1 - a) * rA) by A5, RVSUM_1:39
.= ((1 * rB) - (a * rB)) - ((1 - a) * rA) by EUCLID_4:3
.= ((1 - a) * rB) - ((1 - a) * rA) by EUCLIDLP:11
.= (1 - a) * (rB - rA) by EUCLIDLP:12 ;
then |.(B - C).| = |.(1 - a).| * |.(B - A).| by EUCLID:11
.= |.(1 - a).| * |.(A - B).| by EUCLID_6:43 ;
then |.a.| = |.(1 - a).| by A6, A2, A4, XCMPLX_1:5;
then a = 1 / 2 by Th2;
then C = ((1 - (1 / 2)) * A) + ((1 / 2) * B) by A5;
then C in { (((1 - r) * A) + (r * B)) where r is Real : ( 0 <= r & r <= 1 ) } ;
hence C in LSeg (A,B) by RLTOPSP1:def 2; :: thesis: verum

end;

end;