let n be Nat; :: thesis: ( n + 1 is Prime implies SetPrimes (n + 1) = (SetPrimes n) \/ {(n + 1)} )
A1: SetPrimes (n + 1) = SetPrimes /\ ((Seg n) \/ {(n + 1)}) by FINSEQ_1:9
.= (SetPrimes n) \/ (SetPrimes /\ {(n + 1)}) by XBOOLE_1:23 ;
assume n + 1 is Prime ; :: thesis: SetPrimes (n + 1) = (SetPrimes n) \/ {(n + 1)}
then n + 1 in SetPrimes by NEWTON:def 6;
hence SetPrimes (n + 1) = (SetPrimes n) \/ {(n + 1)} by A1, ZFMISC_1:46; :: thesis: verum