let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C are_mutually_distinct & C in LSeg (A,B) implies |.(A - B).| = |.(A - C).| + |.(C - B).| )
assume that
A1: A,B,C are_mutually_distinct and
A2: C in LSeg (A,B) ; :: thesis: |.(A - B).| = |.(A - C).| + |.(C - B).|
|.(B - A).| ^2 = ((|.(A - C).| ^2) + (|.(B - C).| ^2)) - (((2 * |.(A - C).|) * |.(B - C).|) * (cos (angle (A,C,B)))) by EUCLID_6:7
.= ((|.(A - C).| ^2) + (|.(B - C).| ^2)) - (((2 * |.(A - C).|) * |.(B - C).|) * (- 1)) by A1, A2, SIN_COS:77, EUCLID_6:8
.= ((|.(A - C).| ^2) + ((2 * |.(A - C).|) * |.(B - C).|)) + (|.(B - C).| ^2)
.= (|.(A - C).| + |.(B - C).|) ^2 by SQUARE_1:4 ;
then A3: ( |.(B - A).| = |.(A - C).| + |.(B - C).| or |.(B - A).| = - (|.(A - C).| + |.(B - C).|) ) by SQUARE_1:40;
( |.(B - A).| >= 0 & |.(A - C).| >= 0 & |.(B - C).| >= 0 & not |.(B - A).| = 0 & not |.(A - C).| = 0 & not |.(B - C).| = 0 ) by A1, EUCLID_6:42;
then |.(A - B).| = |.(A - C).| + |.(B - C).| by A3, EUCLID_6:43;
hence |.(A - B).| = |.(A - C).| + |.(C - B).| by EUCLID_6:43; :: thesis: verum