R:(T
TProp), x,y,z:T. (x (R^*) y) 
(y (R^*) z) (x (R^*) z)R:(TTProp), m,n:
, x,y,z:T. (x R^m y) (y R^n z) (x R^m+n z)| Theorem | Name |
| R:(TTProp), x,y,z:T. (x (R^*) y) (y (R^*) z) (x (R^*) z) | [rel_star_transitivity] |
| cites the following: | |
| R:(TTProp), m,n:, x,y,z:T. (x R^m y) (y R^n z) (x R^m+n z) | [rel_exp_add] |