theorem Th6: :: SIN_COS4:6

for th being Real st cos th <> 0 holds
sin th = (cos th) * (tan th)