theorem :: XPRIMES0:800

not 800 is prime