theorem Th39: :: EUCLID12:52

for A, B, C being Point of (TOP-REAL 2)
for L1 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| holds
ex L2 being Element of line_of_REAL 2 st
( C in L2 & L1 _|_ L2 )