theorem :: NEWTON:77

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