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

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