theorem Th40: :: EUCLID12:55

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