theorem Th19: :: EUCLID12:26

for A, B being Point of (TOP-REAL 2) ex C being Point of (TOP-REAL 2) st
( C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| )