assume A1: SetPrimes is finite ; :: thesis: contradiction
then reconsider SP = SetPrimes as finite set ;
consider n being Nat such that
A2: SetPrimes , Seg n are_equipotent by A1, FINSEQ_1:56;
card SetPrimes = card (Seg n) by A2, CARD_1:5;
then card SetPrimes = card n by FINSEQ_1:55;
then A3: card SP = n ;
set p = primenumber (n + 1);
set SPp = SetPrimenumber (primenumber (n + 1));
A4: n + 1 = card (SetPrimenumber (primenumber (n + 1))) by Def8;
card (SetPrimenumber (primenumber (n + 1))) <= card SP by Th68, NAT_1:43;
hence contradiction by A3, A4, NAT_1:13; :: thesis: verum