let O, A, B be Point of (TOP-REAL 2); ( O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| implies ( |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| & |.(O - A).| = 1 ) )
assume that
A1:
O = |[0,0]|
and
A2:
A = |[0,1]|
and
A3:
B = |[((sqrt 3) / 2),(1 / 2)]|
; ( |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| & |.(O - A).| = 1 )
A4:
( A `1 = 0 & A `2 = 1 & O `1 = 0 & O `2 = 0 & B `1 = (sqrt 3) / 2 & B `2 = 1 / 2 )
by A1, A2, A3, EUCLID:52;
then A5:
A - O = |[(0 - 0),(1 - 0)]|
by EUCLID:61;
( 0 ^2 = 0 * 0 & 1 ^2 = 1 * 1 )
by SQUARE_1:def 1;
then A6:
|.A.| = sqrt ((0 * 0) + (1 * 1))
by A4, JGRAPH_1:30;
A7: B - O =
|[(((sqrt 3) / 2) - 0),((1 / 2) - 0)]|
by A4, EUCLID:61
.=
|[((sqrt 3) / 2),(1 / 2)]|
;
A - B = |[(0 - ((sqrt 3) / 2)),(1 - (1 / 2))]|
by A4, EUCLID:61;
then
( (A - B) `1 = - ((sqrt 3) / 2) & (A - B) `2 = 1 / 2 )
by EUCLID:52;
then A8:
|.(A - B).| = sqrt (((- ((sqrt 3) / 2)) ^2) + ((1 / 2) ^2))
by JGRAPH_1:30;
A9:
(- ((sqrt 3) / 2)) ^2 = (- ((sqrt 3) / 2)) * (- ((sqrt 3) / 2))
by SQUARE_1:def 1;
A10:
(1 / 2) ^2 = (1 / 2) * (1 / 2)
by SQUARE_1:def 1;
(sqrt 3) ^2 = 3
by SQUARE_1:def 2;
then A11:
(((sqrt 3) * (sqrt 3)) / 2) / 2 = (3 / 2) / 2
by SQUARE_1:def 1;
|.(O - B).| = |.(B - O).|
by EUCLID_6:43;
hence
( |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| & |.(O - A).| = 1 )
by EUCLID_6:43, A6, A5, A2, A9, A10, A8, A11, A7, Lm2; verum