theorem Th7: :: SIN_COS5:7

for x being Real holds
( cos (2 * x) = ((cos x) ^2) - ((sin x) ^2) & cos (2 * x) = (2 * ((cos x) ^2)) - 1 & cos (2 * x) = 1 - (2 * ((sin x) ^2)) )