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