let x be Real; :: thesis: (sin x) ^2 = (1 - (cos (2 * x))) / 2
(1 - (cos (2 * x))) / 2 = (1 - (1 - (2 * ((sin x) ^2)))) / 2 by Th7
.= (((sin x) ^2) * 2) / 2 ;
hence (sin x) ^2 = (1 - (cos (2 * x))) / 2 ; :: thesis: verum