m) 
(A ~ k) m = k
f:(m
k). Inj(m; k; f)) m
kf:(AB). Bij(A; B; f)) 
(A ~ B)| Rank | Theorem | Name |
| 3 | m) (A ~ k) m = k | [counting_is_unique] |
| cites the following: | ||
| 2 | f:(mk). Inj(m; k; f)) mk | [inj_imp_le] |
| 2 | f:(AB). Bij(A; B; f)) (A ~ B) | [bij_iff_1_1_corr_version2] |
| 1 | [one_one_corr_is_equiv_rel] |