theorem Th4: :: SIN_COS4:4

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