theorem LePrimeSelf: :: PRIMRECI:11

for n being Nat holds n <= primenumber n