let x be Real; :: thesis: ( x > 0 implies sinh x >= 0 )
assume A1: x > 0 ; :: thesis: sinh x >= 0
then x + (- x) > 0 + (- x) by XREAL_1:8;
then A2: exp_R . (- x) <= 1 by SIN_COS:53;
exp_R . x >= 1 by A1, SIN_COS:52;
then (exp_R . x) - (exp_R . (- x)) >= 1 - 1 by A2, XREAL_1:13;
then ((exp_R . x) - (exp_R . (- x))) / 2 >= 0 by XREAL_1:136;
then sinh . x >= 0 by SIN_COS2:def 1;
hence sinh x >= 0 by SIN_COS2:def 2; :: thesis: verum