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 & x' is prime ) by A2, Def7;
then ( x' < q & x' is prime ) by A1, XXREAL_0:2;
hence x in SetPrimenumber q by Def7; :: thesis: verum