R:(A
AProp).
Thm* (EquivRel x,y:A. R(x;y))
Thm*
Thm* (
x:A. R(x;x) & (y:A. R(x;y) 
R(y;x) & (z:A. R(y;z) R(x;z)))) InvFuns(B;A;g;f)| Theorem | Name |
| [one_one_corr_is_equiv_rel] | |
| cites the following: | |
| R:(AAProp).
Thm* (EquivRel x,y:A. R(x;y)) Thm*
Thm* ( x:A. R(x;x) & (y:A. R(x;y) R(y;x) & (z:A. R(y;z) R(x;z)))) | [equivrel_characterization] |
| InvFuns(B;A;g;f) | [inv_funs_2_sym] |