theorem :: XPRIMES0:80

not 80 is prime