let A, B, C be 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).|
let L1, L2 be 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 D be Point of (TOP-REAL 2); ( 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
; |.(D - A).| = |.(D - B).|
per cases
( D = C or D <> C )
;
suppose A9:
D <> C
;
|.(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;
verum end;