theorem Cosik1: :: MOEBIUS2:21

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