for n, m being Nat holds
( n < m iff primenumber n < primenumber m )