let A, B be Point of (TOP-REAL 2); :: thesis: ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| )

take C = (1 / 2) * (A + B); :: thesis: ( C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| )

thus C in LSeg (A,B) by RLTOPSP1:69; :: thesis: |.(A - C).| = (1 / 2) * |.(A - B).|

thus |.(A - C).| = (1 / 2) * |.(A - B).| by Th18; :: thesis: verum

( C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| )

take C = (1 / 2) * (A + B); :: thesis: ( C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| )

thus C in LSeg (A,B) by RLTOPSP1:69; :: thesis: |.(A - C).| = (1 / 2) * |.(A - B).|

thus |.(A - C).| = (1 / 2) * |.(A - B).| by Th18; :: thesis: verum