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).|

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 )
;

end;

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;.= |.(B - C).| by A3, A4, Th30

.= |.(D - B).| by A8, EUCLID_6:43 ;

hence |.(D - A).| = |.(D - B).| ; :: thesis: verum

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;( 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