set O = |[0,0]|;
set A = |[0,1]|;
set B = |[((sqrt 3) / 2),(1 / 2)]|;
set a = |.(|[((sqrt 3) / 2),(1 / 2)]| - |[0,0]|).|;
set b = |.(|[0,1]| - |[0,0]|).|;
set c = |.(|[0,1]| - |[((sqrt 3) / 2),(1 / 2)]|).|;
( |.(|[0,0]| - |[0,1]|).| = |.(|[0,0]| - |[((sqrt 3) / 2),(1 / 2)]|).| & |.(|[0,0]| - |[0,1]|).| = |.(|[0,1]| - |[((sqrt 3) / 2),(1 / 2)]|).| & |.(|[0,0]| - |[0,1]|).| = 1 ) by Lm3;
then A1: ( |.(|[0,1]| - |[0,0]|).| = 1 & |.(|[0,1]| - |[((sqrt 3) / 2),(1 / 2)]|).| = 1 & |.(|[((sqrt 3) / 2),(1 / 2)]| - |[0,0]|).| = 1 ) by EUCLID_6:43;
1 ^2 = 1 * 1 by SQUARE_1:def 1
.= 1 ;
then 1 = (1 + 1) - (((2 * 1) * 1) * (cos (angle (|[((sqrt 3) / 2),(1 / 2)]|,|[0,0]|,|[0,1]|)))) by A1, EUCLID_6:7;
hence cos (PI / 3) = 1 / 2 by Lm1, Lm6; :: thesis: verum