for x being Real st x >= 0 holds
tanh x >= 0