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

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