theorem :: XPRIMES0:9

not 9 is prime