for m being Nat holds SetPrimenumber m c= Seg m