dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
hence Swap (R,x,y) is finite by FINSET_1:10; :: thesis: verum