f:(A
B). Bij(A; B; f) 
(
g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))f:(AB), g:(BA). InvFuns(A; B; f; g) InvFuns(B; A; g; f)f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A; B; f; g))f:(AB), g:(BA). InvFuns(A; B; f; g) Bij(A; B; f)| Rank | Theorem | Name |
| 2 | Thm* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g)) | [inverse-biject] |
| cites | ||
| 0 | Thm* f:(AB), g:(BA). InvFuns(A; B; f; g) InvFuns(B; A; g; f) | [inv_funs_sym] |
| 1 | Thm* f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A; B; f; g)) | [bij_imp_exists_inv] |
| 0 | Thm* f:(AB), g:(BA). InvFuns(A; B; f; g) Bij(A; B; f) | [fun_with_inv_is_bij] |