cos (PI / 6) = cos ((PI / 2) - (PI / 3))
.= (sqrt 3) / 2 by Thm9, SIN_COS:79 ;
hence cos (PI / 6) = (sqrt 3) / 2 ; :: thesis: verum