theorem Th76: :: NEWTON:76

for f being Prime
for g being Nat st f < g holds
(SetPrimenumber f) \/ {f} c= SetPrimenumber g