set O = euc2cpx |[0,0]|;
set A = euc2cpx |[0,1]|;
set B = euc2cpx |[((sqrt 3) / 2),(1 / 2)]|;
( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 & |[0,1]| `1 = 0 & |[0,1]| `2 = 1 & |[((sqrt 3) / 2),(1 / 2)]| `1 = (sqrt 3) / 2 & |[((sqrt 3) / 2),(1 / 2)]| `2 = 1 / 2 )
by EUCLID:52;
then A1:
( euc2cpx |[0,0]| = 0 + (0 * <i>) & euc2cpx |[0,1]| = 0 + (1 * <i>) & euc2cpx |[((sqrt 3) / 2),(1 / 2)]| = ((sqrt 3) / 2) + ((1 / 2) * <i>) )
by EUCLID_3:def 2;
A2:
Arg ((- 1) * <i>) = (3 / 2) * PI
by COMPTRIG:38;
(euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|) = ((sqrt 3) / 2) + ((- (1 / 2)) * <i>)
by A1;
then A3:
( Re ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|)) = (sqrt 3) / 2 & Im ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|)) = - (1 / 2) )
by COMPLEX1:12;
sqrt 3 > 0
by SQUARE_1:25;
then
Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|)) in ].((3 / 2) * PI),(2 * PI).[
by A3, COMPTRIG:44;
then
( (3 / 2) * PI < Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|)) & Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|)) < 2 * PI )
by XXREAL_1:4;
then A4:
( ((3 / 2) * PI) - ((3 / 2) * PI) < (Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|))) - ((3 / 2) * PI) & (Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|))) - ((3 / 2) * PI) < (2 * PI) - ((3 / 2) * PI) )
by XREAL_1:14;
set th = (Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|))) - (Arg ((euc2cpx |[0,0]|) - (euc2cpx |[0,1]|)));
PI in ].0,4.[
by SIN_COS:def 28;
then A5:
0 < PI
by XXREAL_1:4;
( (Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|))) - (Arg ((euc2cpx |[0,0]|) - (euc2cpx |[0,1]|))) < (1 / 2) * PI & (1 / 2) * PI < PI )
by A1, A2, A4, A5, XREAL_1:157;
then A6:
not PI <= (Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|))) - (Arg ((euc2cpx |[0,0]|) - (euc2cpx |[0,1]|)))
by XXREAL_0:2;
angle ((euc2cpx |[0,0]|),(euc2cpx |[0,1]|),(euc2cpx |[((sqrt 3) / 2),(1 / 2)]|)) = (Arg ((euc2cpx |[((sqrt 3) / 2),(1 / 2)]|) - (euc2cpx |[0,1]|))) - (Arg ((euc2cpx |[0,0]|) - (euc2cpx |[0,1]|)))
by A1, A2, A4, COMPLEX2:def 4;
hence
angle (|[0,0]|,|[0,1]|,|[((sqrt 3) / 2),(1 / 2)]|) < PI
by A6, EUCLID_3:def 4; verum