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