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