tan (PI / 3) = ((sqrt 3) / 2) / (1 / 2) by Thm8, Thm9, SIN_COS4:def 1
.= sqrt 3 ;
hence tan (PI / 3) = sqrt 3 ; :: thesis: verum