theorem Th5: :: SIN_COS4:5

for th being Real holds (cos th) * (cos th) = 1 - ((sin th) * (sin th))