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)

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

end;

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

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