let x be Nat; :: according to NUMBER05:def 3 :: thesis: ( 181 < x & x < 181 + 10 implies not x is prime )
assume ( 181 < x & x < 181 + 10 ) ; :: thesis: not x is prime
then ( 181 < x & x < 190 + 1 ) ;
then ( 181 + 1 <= x & x <= 190 ) by NAT_1:13;
then not not x = 182 & ... & not x = 190 ;
hence not x is prime by XPRIMES0:182, XPRIMES0:183, XPRIMES0:184, XPRIMES0:185, XPRIMES0:186, XPRIMES0:187, XPRIMES0:188, XPRIMES0:189, XPRIMES0:190; :: thesis: verum