let n, m, l be natural number ; :: thesis: {n,m,l} is finite Subset of NAT
reconsider Y = {m,l} as finite Subset of NAT by Th5;
reconsider X = {n} as finite Subset of NAT by Th4;
{n,m,l} = X \/ Y by ENUMSET1:42;
hence {n,m,l} is finite Subset of NAT ; :: thesis: verum