let n be Nat; :: thesis: n <= primenumber n
SetPrimenumber (primenumber n) c= Seg (primenumber n) by NEWTON:73;
then card (SetPrimenumber (primenumber n)) <= card (Seg (primenumber n)) by CARD_1:11, FIELD_5:3;
hence n <= primenumber n by NEWTON:def 8; :: thesis: verum