theorem :: XPRIMES0:902

not 902 is prime