let n, m, l be Nat; :: 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:2;
hence {n,m,l} is finite Subset of NAT ; :: thesis: verum