theorem Th27: :: COMPTRIG:27

for x being Real holds
( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] )