m,n,x:
. m<n & n
x 
m<xThm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all(p:hnum. implies(and(lt(m,n),le(n,p)),lt(m,p)))))| Theorem | Name |
| m,n,x:. m<n & nx m<x | [less_less_eq_trans] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. all(p:hnum. implies(and(lt(m,n),le(n,p)),lt(m,p))))) | [hless_less_eq_trans] |