theorem Th15: :: SIN_COS2:15

for p being Real holds
( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 )