let th be Real; :: thesis: (cos th) * (cos th) = 1 - ((sin th) * (sin th))
(cos th) * (cos th) = ((cos th) * (cos th)) + (1 - 1)
.= ((cos th) * (cos th)) + (1 - (- (- (((sin th) * (sin th)) + ((cos th) * (cos th)))))) by SIN_COS:29
.= 1 - ((sin th) * (sin th)) ;
hence (cos th) * (cos th) = 1 - ((sin th) * (sin th)) ; :: thesis: verum