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

assume that

A1: C in LSeg (A,B) and

A2: |.(A - C).| = (1 / 2) * |.(A - B).| ; :: thesis: |.(B - C).| = (1 / 2) * |.(A - B).|

|.(A - B).| = |.(A - C).| + |.(C - B).| by A1, Th8;

hence |.(B - C).| = (1 / 2) * |.(A - B).| by A2, EUCLID_6:43; :: thesis: verum

assume that

A1: C in LSeg (A,B) and

A2: |.(A - C).| = (1 / 2) * |.(A - B).| ; :: thesis: |.(B - C).| = (1 / 2) * |.(A - B).|

|.(A - B).| = |.(A - C).| + |.(C - B).| by A1, Th8;

hence |.(B - C).| = (1 / 2) * |.(A - B).| by A2, EUCLID_6:43; :: thesis: verum