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).|
per cases ( A,B,C are_mutually_distinct or not A,B,C are_mutually_distinct ) ;
suppose A,B,C are_mutually_distinct ; :: thesis: |.(A - B).| = |.(A - C).| + |.(C - B).|
hence |.(A - B).| = |.(A - C).| + |.(C - B).| by A1, EUCLID10:57; :: thesis: verum
end;
suppose not A,B,C are_mutually_distinct ; :: thesis: |.(A - B).| = |.(A - C).| + |.(C - B).|
per cases then ( A = B or C = B or C = A ) ;
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;
suppose C = B ; :: thesis: |.(A - B).| = |.(A - C).| + |.(C - B).|
then ( |.(C - B).| = |.(B - B).| & |.(A - C).| = |.(A - B).| & |.(B - B).| = 0 ) by EUCLID_6:42;
hence |.(A - B).| = |.(A - C).| + |.(C - B).| ; :: thesis: verum
end;
suppose C = A ; :: thesis: |.(A - B).| = |.(A - C).| + |.(C - B).|
then ( |.(A - C).| = |.(C - C).| & |.(A - B).| = |.(C - B).| & |.(C - C).| = 0 ) by EUCLID_6:42;
hence |.(A - B).| = |.(A - C).| + |.(C - B).| ; :: thesis: verum
end;
end;
end;
end;