defpred S₁[ Nat] means ex m being Nat st
( $1 = card (SetPrimenumber m) & m is Prime );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
given m being Nat such that A2: n = card (SetPrimenumber m) and
A3: m is Prime ; :: thesis: S₁[n + 1]
defpred S₂[ Nat] means ( $1 is prime & $1 > m );
A4: not m in SetPrimenumber m by Def7;
A5: ex k being Nat st S₂[k]

proof

ex p being Prime st p > m by Th72;
hence ex k being Nat st S₂[k] ; :: thesis: verum

end;

consider k being Nat such that
A6: ( S₂[k] & ( for l being Nat st S₂[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;

per cases ( s = m or s < m ) by A10, XXREAL_0:1;

suppose s = m ; :: thesis: s in (SetPrimenumber m) \/ {m}

then s in {m} by TARSKI:def 1;
hence s in (SetPrimenumber m) \/ {m} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A11: s < m ; :: thesis: s in (SetPrimenumber m) \/ {m}

A12: SetPrimenumber m c= (SetPrimenumber m) \/ {m} by XBOOLE_1:7;
s in SetPrimenumber m by A9, A11, Def7;
hence s in (SetPrimenumber m) \/ {m} by A12; :: thesis: verum

end;

end;

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: S₁[ 0 ] by CARD_1:27, INT_2:28;
for n being Nat holds S₁[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 b₁ being prime Element of NAT st n = card (SetPrimenumber b₁) by A14, A15; :: thesis: verum