the_w:World, e:E. first(e) 
(t':
. t'<time(e) 
isnull(a(loc(e);t')))the_w:World, i:Id, t:. first(<i,t>) 
| Theorem | Name |
| the_w:World, e:E. first(e) (t':. t'<time(e) isnull(a(loc(e);t'))) | [assert-w-first] |
| cites the following: | |
| the_w:World, i:Id, t:. first(<i,t>) | [w-first-aux] |