L1,L2:V List, s:Traversal. L1-- > *L2 
dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s)A,B,C:V List. A-- > *B B-- > *C A-- > *C| Theorem | Name |
| Thm* For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s) | [dfl-traversal-connect] |
| cites | |
| Thm* For any graph
A,B,C:V List. A-- > *B B-- > *C A-- > *C | [list-list-connect_transitivity] |