let O, A, B be Point of (TOP-REAL 2); ( O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| implies ( angle (B,O,A) = angle (O,A,B) & angle (O,A,B) = angle (A,B,O) ) )
assume that
A1:
O = |[0,0]|
and
A2:
A = |[0,1]|
and
A3:
B = |[((sqrt 3) / 2),(1 / 2)]|
; ( angle (B,O,A) = angle (O,A,B) & angle (O,A,B) = angle (A,B,O) )
A4:
( |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| )
by A1, A2, A3, Lm3;
then A5:
( |.(O - A).| = |.(B - O).| & |.(A - O).| = |.(O - B).| & |.(O - A).| = |.(B - A).| & |.(A - O).| = |.(A - B).| )
by EUCLID_6:43;
( O <> A & A <> B & O <> B )
by A1, A2, A3, Lm4;
hence
( angle (B,O,A) = angle (O,A,B) & angle (O,A,B) = angle (A,B,O) )
by A4, A5, EUCLID_6:16; verum