for n being Nat holds (SetPrimenumber n) \/ {n} is finite ;