let x be Nat; :: according to NUMBER05:def 4 :: thesis: ( 10 * 53 < x & x < 10 * (53 + 1) implies not x is prime )
assume ( 10 * 53 < x & x < 10 * (53 + 1) ) ; :: thesis: not x is prime
then ( 530 < x & x < 539 + 1 ) ;
then ( 530 + 1 <= x & x <= 539 ) by NAT_1:13;
then not not x = 531 & ... & not x = 539 ;
hence not x is prime by XPRIMES0:531, XPRIMES0:532, XPRIMES0:533, XPRIMES0:534, XPRIMES0:535, XPRIMES0:536, XPRIMES0:537, XPRIMES0:538, XPRIMES0:539; :: thesis: verum