n,m:
. n
m & mn 
n = m
n:hnum. all(m:hnum. implies(and(le(n,m),le(m,n)),equal(n,m))))| Theorem | Name |
| n,m:. nm & mn n = m | [less_equal_antisym] |
| cites the following: | |
| n:hnum. all(m:hnum. implies(and(le(n,m),le(m,n)),equal(n,m)))) | [hless_equal_antisym] |