sin (PI / 6) = sin ((PI / 2) - (PI / 3))
.= 1 / 2 by Thm8, SIN_COS:79 ;
hence sin (PI / 6) = 1 / 2 ; :: thesis: verum