(
a onto
b)) 
((b inj a))
f:(a onto b). (
y.least x:. f(x)=
y) b inj a| Rank | Theorem | Name |
| 5 | (a onto b)) ((b inj a)) | [nsub_surj_imp_a_rev_inj2] |
| cites the following: | ||
| 4 | f:(a onto b). (y.least x:. f(x)=y) b inj a | [nsub_surj_imp_a_rev_inj] |