a,b',b:
. b = b'+1 
({a...b'} ~ {a..b
})x:A. B(x) 
B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) })| Rank | Theorem | Name |
| 3 | a,b',b:. b = b'+1 ({a...b'} ~ {a..b}) | [intiseg_intseg] |
| cites the following: | ||
| 2 | x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred2] |