f:(
a onto
b). Surj(a; b; f)f:(A onto B), a:. a onto A 
(B Discrete) Surj(A; B; f)| Rank | Theorem | Name |
| 3 | f:(a onto b). Surj(a; b; f) | [surjection_type_nsub_surjection] |
| cites the following: | ||
| 2 | f:(A onto B), a:. a onto A (B Discrete) Surj(A; B; f) | [surjection_type_surjection] |