consider C being Point of (TOP-REAL 2) such that
A1: C in LSeg (A,B) and
A2: |.(A - C).| = half_length (A,B) by Th19;
take C ; :: thesis: ex C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & C = C & |.(A - C).| = half_length (A,B) )
thus ex C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & C = C & |.(A - C).| = half_length (A,B) ) by A1, A2; :: thesis: verum