:: deftheorem Def1 defines the_midpoint_of_the_segment EUCLID12:def 3 :

for A, B, b_{3} being Point of (TOP-REAL 2) holds

( b_{3} = the_midpoint_of_the_segment (A,B) iff ex C being Point of (TOP-REAL 2) st

( C in LSeg (A,B) & b_{3} = C & |.(A - C).| = half_length (A,B) ) );

for A, B, b

( b

( C in LSeg (A,B) & b