D,D':Dsys, P:({es:ES| es is an event system of D }
Prop{i'}).
Thm* D realizes es.P(es)
D 
D' D' realizes es.P(es)D1,D2,D3:Dsys. D1 D2 D2 D3 D1 D3| Rank | Theorem | Name |
| 9 | D,D':Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
Thm* D realizes es.P(es) D D' D' realizes es.P(es) | [realizes-monotone-wrt-sub] |
| cites the following: | ||
| 8 | D1,D2,D3:Dsys. D1 D2 D2 D3 D1 D3 | [d-sub_transitivity] |