let x be Nat; :: according to NUMBER05:def 4 :: thesis: ( 10 * 20 < x & x < 10 * (20 + 1) implies not x is prime )
assume ( 10 * 20 < x & x < 10 * (20 + 1) ) ; :: thesis: not x is prime
then ( 200 < x & x < 209 + 1 ) ;
then ( 200 + 1 <= x & x <= 209 ) by NAT_1:13;
then not not x = 201 & ... & not x = 209 ;
hence not x is prime by XPRIMES0:201, XPRIMES0:202, XPRIMES0:203, XPRIMES0:204, XPRIMES0:205, XPRIMES0:206, XPRIMES0:207, XPRIMES0:208, XPRIMES0:209; :: thesis: verum