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