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