theorem CardSetPrime1: :: PRIMRECI:10

for n being Nat
for p being Prime st p < n holds
(card (SetPrimenumber p)) + 1 <= card (SetPrimenumber n)