D:Dsys, P:({es:ES| es is an event system of D }
Prop{i'}).
Thm* D realizes es.P(es)
Prop{i''}A,B:Dsys. A 
B 
(w:World. PossibleWorld(B;w) PossibleWorld(A;w))| Rank | Theorem | Name |
| 3 | D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
Thm* D realizes es.P(es) Prop{i''} | [d-realizes_wf] |
| cites the following: | ||
| 2 | A,B:Dsys. A B (w:World. PossibleWorld(B;w) PossibleWorld(A;w)) | [possible-world-monotonic] |