let x be Real; :: thesis: ( sech x <= 1 & 0 < sech x & sech 0 = 1 )
A1: 2 / 2 >= 2 / ((exp_R x) + (exp_R (- x))) by Lm9, XREAL_1:183;
0 < cosh . x by SIN_COS2:15;
then 0 < cosh x by SIN_COS2:def 4;
then A2: 0 < 1 / (cosh x) by XREAL_1:139;
sech 0 = 1 / 1 by Lm1, SIN_COS5:def 2
.= 1 ;
hence ( sech x <= 1 & 0 < sech x & sech 0 = 1 ) by A2, A1, SIN_COS5:36, SIN_COS5:def 2; :: thesis: verum