let x be Nat; :: according to NUMBER05:def 4 :: thesis: ( 10 * 51 < x & x < 10 * (51 + 1) implies not x is prime )
assume ( 10 * 51 < x & x < 10 * (51 + 1) ) ; :: thesis: not x is prime
then ( 510 < x & x < 519 + 1 ) ;
then ( 510 + 1 <= x & x <= 519 ) by NAT_1:13;
then not not x = 511 & ... & not x = 519 ;
hence not x is prime by XPRIMES0:511, XPRIMES0:512, XPRIMES0:513, XPRIMES0:514, XPRIMES0:515, XPRIMES0:516, XPRIMES0:517, XPRIMES0:518, XPRIMES0:519; :: thesis: verum