let n be Nat; :: thesis: ( n + 1 is not Prime implies SetPrimes (n + 1) = SetPrimes n )
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 not Prime ; :: thesis: SetPrimes (n + 1) = SetPrimes n
then not n + 1 in SetPrimes by NEWTON:def 6;
then SetPrimes /\ {(n + 1)} = {} by XBOOLE_0:def 7, ZFMISC_1:50;
hence SetPrimes (n + 1) = SetPrimes n by A1; :: thesis: verum