theorem :: SIN_COS2:37

for p being Real holds cosh . p >= 1