let n be Nat; :: thesis: for p being Prime st p < n holds
(card (SetPrimenumber p)) + 1 <= card (SetPrimenumber n)
let p be Prime; :: thesis: ( p < n implies (card (SetPrimenumber p)) + 1 <= card (SetPrimenumber n) )
assume p < n ; :: thesis: (card (SetPrimenumber p)) + 1 <= card (SetPrimenumber n)
then card ((SetPrimenumber p) \/ {p}) <= card (SetPrimenumber n) by NEWTON:76, NAT_1:43;
hence (card (SetPrimenumber p)) + 1 <= card (SetPrimenumber n) by NEWTON:74, CARD_2:41; :: thesis: verum