R1,R2:(T
TProp). (x,y:T. R1(x,y) 
R2(x,y)) 
Graph(x,y:T. R1(x,y)) 
Graph(x,y:T. R2(x,y))| Theorem | Name |
| 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] |
| cites | |
| Thm* Bij(T; T; Id) | [identity-biject] |