let n be Nat; :: thesis: not n + 1 in SetPrimes n
assume n + 1 in SetPrimes n ; :: thesis: contradiction
then n + 1 in Seg n by XBOOLE_0:def 4;
then n + 1 <= n by FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum