B, same_range_sep(A; B)
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))))| Theorem | Name |
| B, same_range_sep(A; B) | [same_range_sep_eqv] |
| 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] |