let x be Nat; :: according to NUMBER05:def 4 :: thesis: ( 10 * 62 < x & x < 10 * (62 + 1) implies not x is prime )
assume ( 10 * 62 < x & x < 10 * (62 + 1) ) ; :: thesis: not x is prime
then ( 620 < x & x < 629 + 1 ) ;
then ( 620 + 1 <= x & x <= 629 ) by NAT_1:13;
then not not x = 621 & ... & not x = 629 ;
hence not x is prime by XPRIMES0:621, XPRIMES0:622, XPRIMES0:623, XPRIMES0:624, XPRIMES0:625, XPRIMES0:626, XPRIMES0:627, XPRIMES0:628, XPRIMES0:629; :: thesis: verum