theorem Th91: :: SIN_COS6:91
for r being Real st - 1 <= r & r <= 1 holds
cos (arccos r) = r