G:(Id
), to,from:(|G|(IdLnk List)), i:|G|.
Thm* bi-graph(G;to;from)
from(i) 
Edge(G) ListP:(TProp), x:T, L:T List. (y[x / L].P(y)) 
P(x) & (yL.P(y))| Rank | Theorem | Name |
| 3 | G:(Id), to,from:(|G|(IdLnk List)), i:|G|.
Thm* bi-graph(G;to;from) from(i) Edge(G) List | [bi-graph-from_wf] |
| cites the following: | ||
| 2 | P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y)) | [l_all_cons] |