theorem Th3: :: SIN_COS8:3

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