es:ES, e':E. 
e:E. first(e) & e 
e' the_es:ES. Trans x,y:E. x y the_es:ES, j:E. 
first(j) 
(pred(j) <loc j)| Rank | Theorem | Name |
| 2 | es:ES, e':E. e:E. first(e) & e e' | [es-first-exists] |
| cites the following: | ||
| 1 | the_es:ES. Trans x,y:E. x y | [es-le-trans] |
| 0 | the_es:ES, j:E. first(j) (pred(j) <loc j) | [es-pred-locl] |