{x1,x2,x3,x4,x5,x6,x7,x8} is finite

proof

( {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} & {x1} is finite & {x2,x3,x4,x5,x6,x7,x8} is finite ) by ENUMSET1:62;
hence {x1,x2,x3,x4,x5,x6,x7,x8} is finite by Lm2; :: thesis: verum

end;

hence {x1,x2,x3,x4,x5,x6,x7,x8} is finite ; :: thesis: verum