let x be Real; :: thesis: ( cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0 )
cosh . x >= 1 by SIN_COS2:37;
hence ( cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0 ) by SIN_COS2:15, SIN_COS2:16, SIN_COS2:def 2, SIN_COS2:def 4; :: thesis: verum