let A, B, C be Point of (TOP-REAL 2); :: thesis: 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).|
let L1, L2 be Element of line_of_REAL 2; :: thesis: 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).|
let D be Point of (TOP-REAL 2); :: thesis: ( 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 implies |.(D - A).| = |.(D - B).| )
assume that
A1: A <> B and
A2: L1 = Line (A,B) and
A3: C in LSeg (A,B) and
A4: |.(A - C).| = (1 / 2) * |.(A - B).| and
A5: C in L2 and
A6: L1 _|_ L2 and
A7: D in L2 ; :: thesis: |.(D - A).| = |.(D - B).|

per cases ( D = C or D <> C ) ;

suppose A8: D = C ; :: thesis: |.(D - A).| = |.(D - B).|

then |.(D - A).| = (1 / 2) * |.(A - B).| by A4, EUCLID_6:43
.= |.(B - C).| by A3, A4, Th30
.= |.(D - B).| by A8, EUCLID_6:43 ;
hence |.(D - A).| = |.(D - B).| ; :: thesis: verum

end;

suppose A9: D <> C ; :: thesis: |.(D - A).| = |.(D - B).|

A10: A,B,C are_mutually_distinct by A1, A4, Th29;
( C in L1 & A in L1 ) by A3, A2, MENELAUS:12, RLTOPSP1:68;
then A11: ( L1 _|_ L2 & C in L1 /\ L2 & A in L1 & D in L2 & A <> C & D <> C ) by A5, A6, A7, A10, A9, XBOOLE_0:def 4;
( C in L1 & B in L1 ) by A3, A2, MENELAUS:12, RLTOPSP1:68;
then A12: ( L1 _|_ L2 & C in L1 /\ L2 & B in L1 & D in L2 & B <> C & D <> C ) by A6, A7, A10, A9, A5, XBOOLE_0:def 4;
reconsider a1 = |.(D - C).|, b1 = |.(A - C).|, c1 = |.(A - D).| as Real ;
reconsider a2 = |.(D - C).|, b2 = |.(B - C).|, c2 = |.(B - D).| as Real ;
A13: cos (angle (D,C,A)) = 0 by A11, Th38, SIN_COS:77;
A14: cos (angle (D,C,B)) = 0 by A12, Th38, SIN_COS:77;
c1 ^2 = ((a1 ^2) + (b1 ^2)) - (((2 * a1) * b1) * (cos (angle (D,C,A)))) by EUCLID_6:7
.= ((a2 ^2) + (b2 ^2)) - (((2 * a2) * b2) * (cos (angle (D,C,B)))) by A13, A14, A3, A4, Th30
.= c2 ^2 by EUCLID_6:7 ;
then A15: c1 = sqrt (c2 ^2) by SQUARE_1:22
.= c2 by SQUARE_1:22 ;
( |.(A - D).| = |.(D - A).| & |.(B - D).| = |.(D - B).| ) by EUCLID_6:43;
hence |.(D - A).| = |.(D - B).| by A15; :: thesis: verum

end;

end;