{x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} by ENUMSET1:7;
hence {x1,x2,x3,x4,x5} is finite by Lm2; :: thesis: verum