let A, B, C be Point of (TOP-REAL 2); ( |.(A - B).| = |.(A - C).| + |.(C - B).| implies C in LSeg (A,B) )
assume A1:
|.(A - B).| = |.(A - C).| + |.(C - B).|
; 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 )
;
suppose A3:
A <> B
;
C in LSeg (A,B)per cases
( C = A or C = B or ( C <> A & C <> B ) )
;
suppose A4:
(
C <> A &
C <> B )
;
C in LSeg (A,B)set a =
|.(A - B).|;
set b =
|.(C - B).|;
set c =
|.(C - A).|;
|.(A - B).| * |.(C - B).| <> 0
then A5:
(2 * |.(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)
hence
C in LSeg (
A,
B)
by A8, EUCLID_6:11;
verum end; end; end; end;