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