let A, B, C be Point of (TOP-REAL 2); :: thesis: ( C in LSeg (A,B) & |.(A - C).| = |.(B - C).| implies half_length (A,B) = |.(A - C).| )
assume that
A1: C in LSeg (A,B) and
A2: |.(A - C).| = |.(B - C).| ; :: thesis: half_length (A,B) = |.(A - C).|
A3: |.(C - B).| = |.(A - C).| by A2, EUCLID_6:43;
half_length (A,B) = (1 / 2) * (|.(A - C).| + |.(C - B).|) by A1, Th8
.= (1 / 2) * (2 * |.(A - C).|) by A3 ;
hence half_length (A,B) = |.(A - C).| ; :: thesis: verum