for k, m being Nat st k >= m holds
not k in SetPrimenumber m by Def7;