let k,

n,

m,

l be

Nat;

{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
;

verum