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