tan (PI / 6) = (1 / 2) / ((sqrt 3) / 2) by Thm11, Thm12, SIN_COS4:def 1
.= 1 / (sqrt 3) by XCMPLX_1:55 ;
hence tan (PI / 6) = (sqrt 3) / 3 by SQUARE_1:33; :: thesis: verum