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; :: thesis: verum