| | No other cites to report in EventSystems |
|
| event_system_typename | Def event_system_typename() == 6 |
|
| int_seg | Def {i..j } == {k: | i k < j } |
| | | Thm* m,n: . {m..n } Type |
|
| lelt | Def i j < k == i j & j<k |
|
| le | Def A B == B<A |
| | | Thm* i,j: . (i j) Prop |
|
| not | Def A == A  False |
| | | Thm* A:Prop. ( A) Prop |