{x,y,z} is finite

proof

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

end;

hence {x,y,z} is finite ; :: thesis: verum