defpred S1[ Nat] means ex m being Nat st
( $1 = card (SetPrimenumber m) & m is Prime );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
given m being Nat such that A2: n = card (SetPrimenumber m) and
A3: m is Prime ; :: thesis: S1[n + 1]
defpred S2[ Nat] means ( $1 is prime & $1 > m );
A4: not m in SetPrimenumber m by Def7;
A5: ex k being Nat st S2[k]
proof
ex p being Prime st p > m by Th72;
hence ex k being Nat st S2[k] ; :: thesis: verum
end;
consider k being Nat such that
A6: ( S2[k] & ( for l being Nat st S2[l] holds
k <= l ) ) from NAT_1:sch 5(A5);
 take k ; :: thesis: ( n + 1 = card (SetPrimenumber k) & k is Prime )
A7: SetPrimenumber k c= (SetPrimenumber m) \/ {m}
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in SetPrimenumber k or s in (SetPrimenumber m) \/ {m} )
assume A8: s in SetPrimenumber k ; :: thesis: s in (SetPrimenumber m) \/ {m}
then reconsider s = s as Element of NAT ;
A9: s is prime by A8, Def7;
s < k by A8, Def7;
then A10: s <= m by A6, A9;
end;
(SetPrimenumber m) \/ {m} c= SetPrimenumber k by A3, A6, Th76;
then SetPrimenumber k = (SetPrimenumber m) \/ {m} by A7;
hence n + 1 = card (SetPrimenumber k) by A2, A4, CARD_2:41; :: thesis: k is Prime
thus k is Prime by A6; :: thesis: verum
end;
SetPrimenumber 2 = { k where k is Element of NAT : ( k < 2 & k is prime ) } by Lm2;
then A13: S1[ 0 ] by CARD_1:27, INT_2:28;
for n being Nat holds S1[n] from NAT_1:sch 2(A13, A1);
 then consider m being Nat such that
A14: n = card (SetPrimenumber m) and
A15: m is Prime ;
m in NAT by ORDINAL1:def 12;
hence ex b1 being prime Element of NAT st n = card (SetPrimenumber b1) by A14, A15; :: thesis: verum