Theorem | Name |
Thm* G:(Id  ), to,from:(|G| (IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)  ((e from(i))  source(e) = i) | [edge-from] |
cites the following: |
Thm* L:A List, x:A. (A r B)  (x L)  (x L) | [l_member_subtype] |
Thm* T:(Id  ), to,from:(|T| (IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)  source(u) |T| | [src-edge] |
Thm* T:(Id  ), to,from:(|T| (IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)  destination(u) |T| | [dst-edge] |