R:(T
TProp), x,y,z:T. (x R y) 
(y (R^*) z) (x (R^*) z)R:(TTProp), x,y:T. (x R y) (x (R^*) y)R:(TTProp), x,y,z:T. (x (R^*) y) (y (R^*) z) (x (R^*) z)| Rank | Theorem | Name |
| 2 | R:(TTProp), x,y,z:T. (x R y) (y (R^*) z) (x (R^*) z) | [rel_star_trans] |
| cites the following: | ||
| 0 | R:(TTProp), x,y:T. (x R y) (x (R^*) y) | [rel_rel_star] |
| 1 | R:(TTProp), x,y,z:T. (x (R^*) y) (y (R^*) z) (x (R^*) z) | [rel_star_transitivity] |