:: deftheorem Def1 defines the_midpoint_of_the_segment EUCLID12:def 3 :
for A, B, b₃ being Point of (TOP-REAL 2) holds
( b₃ = the_midpoint_of_the_segment (A,B) iff ex C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & b₃ = C & |.(A - C).| = half_length (A,B) ) );