let x be Real; :: thesis: ( x >= 0 implies tanh x >= 0 )
A1: cosh x >= 1 by Lm1;
assume A2: x >= 0 ; :: thesis: tanh x >= 0

per cases ( x > 0 or x = 0 ) by A2;

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

then sinh x >= 0 by SIN_COS5:46;
then (sinh x) / (cosh x) >= 0 by A1;
hence tanh x >= 0 by Th1; :: thesis: verum

end;

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

hence tanh x >= 0 by Th1; :: thesis: verum

end;

end;