theorem :: SIN_COS2:44
for p being Real holds
( tanh . p < 1 & tanh . p > - 1 )