for x being Real holds
( sech x <= 1 & 0 < sech x & sech 0 = 1 )