theorem :: EXCHSORT:83
for X, Y being set
for r being b1 -defined b2 -valued Relation holds r is Relation of X,Y