let O, A, B be Point of (TOP-REAL 2); :: thesis: ( O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| & angle (O,A,B) < PI implies angle (B,O,A) = PI / 3 )
assume that
A1: O = |[0,0]| and
A2: A = |[0,1]| and
A3: B = |[((sqrt 3) / 2),(1 / 2)]| and
A4: angle (O,A,B) < PI ; :: thesis: angle (B,O,A) = PI / 3
( A <> O & O <> B & B <> A ) by A1, A2, A3, Lm4;
then A5: ((angle (O,A,B)) + (angle (A,B,O))) + (angle (B,O,A)) = PI by A4, EUCLID_3:47;
( angle (B,O,A) = angle (O,A,B) & angle (O,A,B) = angle (A,B,O) ) by A1, A2, A3, Lm5;
hence angle (B,O,A) = PI / 3 by A5; :: thesis: verum