let p, q be Nat; :: thesis: ( p <= q implies SetPrimenumber p c= SetPrimenumber q )
assume A1: p <= q ; :: thesis: SetPrimenumber p c= SetPrimenumber q
let x be set ; :: 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 x' = x as Element of NAT ;
x' < p by A2, Def7;
then A3: x' < q by A1, XXREAL_0:2;
x' is prime by A2, Def7;
hence x in SetPrimenumber q by A3, Def7; :: thesis: verum