for n being Nat holds SetPrimenumber n = { k where k is Element of NAT : ( k < n & k is prime ) } by Lm2;