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