G:(Id
), to,from:(|G|(IdLnk List)), l:Edge(G).
Thm* bi-graph(G;to;from)
lnk-inv(l) 
Edge(G)l:IdLnk. source(lnk-inv(l)) = destination(l)| Theorem | Name |
| G:(Id), to,from:(|G|(IdLnk List)), l:Edge(G).
Thm* bi-graph(G;to;from) lnk-inv(l) Edge(G) | [inv-is-edge] |
| cites the following: | |
| l:IdLnk. source(lnk-inv(l)) = destination(l) | [lsrc-inv] |