{x,y} = {x} \/ {y} by ENUMSET1:1;
hence {x,y} is finite by Lm2; :: thesis: verum