let A, B, C be Point of (TOP-REAL 2); :: thesis: ( |.(A - B).| = |.(A - C).| + |.(C - B).| implies C in LSeg (A,B) )

assume A1: |.(A - B).| = |.(A - C).| + |.(C - B).| ; :: thesis: C in LSeg (A,B)

then A2: |.(B - A).| = |.(A - C).| + |.(C - B).| by EUCLID_6:43

.= |.(A - C).| + |.(B - C).| by EUCLID_6:43 ;

assume A1: |.(A - B).| = |.(A - C).| + |.(C - B).| ; :: thesis: C in LSeg (A,B)

then A2: |.(B - A).| = |.(A - C).| + |.(C - B).| by EUCLID_6:43

.= |.(A - C).| + |.(B - C).| by EUCLID_6:43 ;

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

end;

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

then
( |.(A - C).| = 0 & |.(C - B).| = 0 )
by A1, EUCLID_6:42;

then ( A = C & C = B ) by EUCLID_6:42;

hence C in LSeg (A,B) by RLTOPSP1:68; :: thesis: verum

end;then ( A = C & C = B ) by EUCLID_6:42;

hence C in LSeg (A,B) by RLTOPSP1:68; :: thesis: verum

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

end;

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

end;

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

set a = |.(A - B).|;

set b = |.(C - B).|;

set c = |.(C - A).|;

|.(A - B).| * |.(C - B).| <> 0

|.(C - A).| = |.(A - B).| - |.(C - B).| by A1, EUCLID_6:43;

then A6: |.(C - A).| ^2 = (|.(A - B).| - |.(C - B).|) * (|.(A - B).| - |.(C - B).|) by SQUARE_1:def 1

.= ((|.(A - B).| * |.(A - B).|) - ((2 * |.(A - B).|) * |.(C - B).|)) + (|.(C - B).| * |.(C - B).|)

.= ((|.(A - B).| ^2) - ((2 * |.(A - B).|) * |.(C - B).|)) + (|.(C - B).| * |.(C - B).|) by SQUARE_1:def 1

.= ((|.(A - B).| ^2) - ((2 * |.(A - B).|) * |.(C - B).|)) + (|.(C - B).| ^2) by SQUARE_1:def 1 ;

|.(C - A).| ^2 = ((|.(A - B).| ^2) + (|.(C - B).| ^2)) - (((2 * |.(A - B).|) * |.(C - B).|) * (cos (angle (A,B,C)))) by EUCLID_6:7;

then A7: ( cos (angle (A,B,C)) = 1 & 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI ) by A6, A5, EUCLID11:2, XCMPLX_1:7;

A,B,C are_mutually_distinct by A3, A4;

then A8: ( angle (B,C,A) = PI or angle (B,A,C) = PI ) by A7, COMPTRIG:61, MENELAUS:8;

not A in LSeg (B,C)

end;set b = |.(C - B).|;

set c = |.(C - A).|;

|.(A - B).| * |.(C - B).| <> 0

proof

then A5:
(2 * |.(A - B).|) * |.(C - B).| <> 0
;
assume
|.(A - B).| * |.(C - B).| = 0
; :: thesis: contradiction

then 0 = (|.(A - B).| * |.(C - B).|) / |.(C - B).|

.= |.(A - B).| by A4, EUCLID_6:42, XCMPLX_1:89 ;

hence contradiction by A3, EUCLID_6:42; :: thesis: verum

end;then 0 = (|.(A - B).| * |.(C - B).|) / |.(C - B).|

.= |.(A - B).| by A4, EUCLID_6:42, XCMPLX_1:89 ;

hence contradiction by A3, EUCLID_6:42; :: thesis: verum

|.(C - A).| = |.(A - B).| - |.(C - B).| by A1, EUCLID_6:43;

then A6: |.(C - A).| ^2 = (|.(A - B).| - |.(C - B).|) * (|.(A - B).| - |.(C - B).|) by SQUARE_1:def 1

.= ((|.(A - B).| * |.(A - B).|) - ((2 * |.(A - B).|) * |.(C - B).|)) + (|.(C - B).| * |.(C - B).|)

.= ((|.(A - B).| ^2) - ((2 * |.(A - B).|) * |.(C - B).|)) + (|.(C - B).| * |.(C - B).|) by SQUARE_1:def 1

.= ((|.(A - B).| ^2) - ((2 * |.(A - B).|) * |.(C - B).|)) + (|.(C - B).| ^2) by SQUARE_1:def 1 ;

|.(C - A).| ^2 = ((|.(A - B).| ^2) + (|.(C - B).| ^2)) - (((2 * |.(A - B).|) * |.(C - B).|) * (cos (angle (A,B,C)))) by EUCLID_6:7;

then A7: ( cos (angle (A,B,C)) = 1 & 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI ) by A6, A5, EUCLID11:2, XCMPLX_1:7;

A,B,C are_mutually_distinct by A3, A4;

then A8: ( angle (B,C,A) = PI or angle (B,A,C) = PI ) by A7, COMPTRIG:61, MENELAUS:8;

not A in LSeg (B,C)

proof

hence
C in LSeg (A,B)
by A8, EUCLID_6:11; :: thesis: verum
assume
A in LSeg (B,C)
; :: thesis: contradiction

then |.(B - C).| = (|.(A - C).| + |.(B - C).|) + |.(A - C).| by A2, Th8

.= (2 * |.(A - C).|) + |.(B - C).| ;

hence contradiction by A4, EUCLID_6:42; :: thesis: verum

end;then |.(B - C).| = (|.(A - C).| + |.(B - C).|) + |.(A - C).| by A2, Th8

.= (2 * |.(A - C).|) + |.(B - C).| ;

hence contradiction by A4, EUCLID_6:42; :: thesis: verum