∀n,m:ℕ. ((natset(n) ∈ natset(m))
n < m)
{ (RWO "setmem-natset" 0 THEN Auto THEN ExRepD) }
1. n : ℕ
2. m : ℕ
3. i : ℕm
4. seteq(natset(n);natset(i))
⊢ n < m
3. n < m
⊢ ∃i:ℕm. seteq(natset(n);natset(i))