| Rank | Theorem | Name |
| 4 | Thm* DivGraph_2  DivGraph_1 | [div-graph-iso] |
| cites |
| 1 | Thm*  G,H,K:Graph. G H   H K G K | [graph-isomorphic_transitivity] |
| 3 | Thm* a,b: , n:  . n a = nb a = b | [mul_cancel_in_eq] |
| 2 | Thm* f:(A  BA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec( b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) Graph(a,a':A. b:B. a' = f(a,b)) | [fun-graph-rel-graph] |
| 3 | Thm* a,b:. ab > 0  a > 0 & b > 0  a < 0 & b < 0 | [pos_mul_arg_bounds] |
| 1 | Thm* R1,R2:(TTProp). (x,y:T. R1(x,y) R2(x,y)) Graph(x,y:T. R1(x,y)) Graph(x,y:T. R2(x,y)) | [rel-graph_functionality] |