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

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

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

per cases
( A,B,C are_mutually_distinct or not A,B,C are_mutually_distinct )
;

end;

suppose
not A,B,C are_mutually_distinct
; :: thesis: |.(A - B).| = |.(A - C).| + |.(C - B).|

end;

per cases then
( A = B or C = B or C = A )
;

end;

suppose
A = B
; :: thesis: |.(A - B).| = |.(A - C).| + |.(C - B).|

then
LSeg (A,B) = {A}
by RLTOPSP1:70;

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

hence |.(A - B).| = |.(A - C).| + |.(C - B).| ; :: thesis: verum

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

hence |.(A - B).| = |.(A - C).| + |.(C - B).| ; :: thesis: verum