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