theorem Th99: :: SIN_COS6:99
for r being Real st - 1 <= r & r <= 1 holds
( 0 <= arccos r & arccos r <= PI )