R:(T
TProp). (Sym x,y:T. x R y) 
(Sym x,y:T. x (R^*) y)R1,R2:(TTProp), x,y:T. R1 => R2 (x (R1^*) y) (x (R2^*) y)| Rank | Theorem | Name |
| 3 | R:(TTProp). (Sym x,y:T. x R y) (Sym x,y:T. x (R^*) y) | [rel_star_symmetric] |
| cites the following: | ||
| 2 | R1,R2:(TTProp), x,y:T. R1 => R2 (x (R1^*) y) (x (R2^*) y) | [rel_star_monotonic] |