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 ;
per cases ( A = B or A <> B ) ;
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;
suppose A3: A <> B ; :: thesis: C in LSeg (A,B)
per cases ( C = A or C = B or ( C <> A & C <> B ) ) ;
suppose ( C = A or C = B ) ; :: thesis: C in LSeg (A,B)
hence C in LSeg (A,B) by RLTOPSP1:68; :: thesis: verum
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
proof
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 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)
proof
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;
hence C in LSeg (A,B) by A8, EUCLID_6:11; :: thesis: verum
end;
end;
end;
end;