let x be real number ; :: 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