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