theorem :: SIN_COS:31

for th being Real holds
( cos 0 = 1 & sin 0 = 0 & cos (- th) = cos th & sin (- th) = - (sin th) ) by Th30;