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