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