theorem Th5: :: NAT_5:5

for n, m being Nat holds {n,m} is finite Subset of NAT