theorem :: XPRIMES0:802

not 802 is prime