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