theorem :: XPRIMES2:9001

9001 is prime