let x be Real; :: thesis: ( x >= 0 implies sinh x >= 0 )
assume A1: x >= 0 ; :: thesis: sinh x >= 0

per cases ( x > 0 or x = 0 ) by A1, XXREAL_0:1;

suppose x > 0 ; :: thesis: sinh x >= 0

hence sinh x >= 0 by Lm4; :: thesis: verum

end;

suppose x = 0 ; :: thesis: sinh x >= 0

hence sinh x >= 0 by SIN_COS2:16, SIN_COS2:def 2; :: thesis: verum

end;

end;