let x be Nat; :: according to NUMBER05:def 4 :: thesis: ( 10 * 32 < x & x < 10 * (32 + 1) implies not x is prime )
assume ( 10 * 32 < x & x < 10 * (32 + 1) ) ; :: thesis: not x is prime
then ( 320 < x & x < 329 + 1 ) ;
then ( 320 + 1 <= x & x <= 329 ) by NAT_1:13;
then not not x = 321 & ... & not x = 329 ;
hence not x is prime by XPRIMES0:321, XPRIMES0:322, XPRIMES0:323, XPRIMES0:324, XPRIMES0:325, XPRIMES0:326, XPRIMES0:327, XPRIMES0:328, XPRIMES0:329; :: thesis: verum