let x be Nat; :: according to NUMBER05:def 3 :: thesis: ( 139 < x & x < 139 + 10 implies not x is prime )
assume ( 139 < x & x < 139 + 10 ) ; :: thesis: not x is prime
then ( 139 < x & x < 148 + 1 ) ;
then ( 139 + 1 <= x & x <= 148 ) by NAT_1:13;
then not not x = 140 & ... & not x = 148 ;
hence not x is prime by XPRIMES0:140, XPRIMES0:141, XPRIMES0:142, XPRIMES0:143, XPRIMES0:144, XPRIMES0:145, XPRIMES0:146, XPRIMES0:147, XPRIMES0:148; :: thesis: verum