(5 * PI) / 6 = PI - (PI / 6) ;
hence sin ((5 * PI) / 6) = 1 / 2 by EUCLID10:1, EUCLID10:17; :: thesis: verum