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

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