theorem Th30: :: SIN_COS:30

for th being Real holds
( cos . 0 = 1 & sin . 0 = 0 & cos . (- th) = cos . th & sin . (- th) = - (sin . th) )