let p be natural Number ; :: thesis: SetPrimenumber p c= SetPrimes
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SetPrimenumber p or x in SetPrimes )
assume A1: x in SetPrimenumber p ; :: thesis: x in SetPrimes
then reconsider x9 = x as Element of NAT ;
x9 is prime by A1, Def7;
hence x in SetPrimes by Def6; :: thesis: verum