let p be natural Number ; :: thesis: SetPrimenumber p c= Seg p
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SetPrimenumber p or x in Seg p )
assume A1: x in SetPrimenumber p ; :: thesis: x in Seg p
then reconsider q = x as Element of NAT ;
q is prime by A1, Def7;
then A2: 1 <= q by INT_2:def 4;
q < p by A1, Def7;
hence x in Seg p by A2; :: thesis: verum