let x be Nat; :: according to NUMBER05:def 3 :: thesis: ( 113 < x & x < 113 + 10 implies not x is prime )
assume ( 113 < x & x < 113 + 10 ) ; :: thesis: not x is prime
then ( 113 < x & x < 122 + 1 ) ;
then ( 113 + 1 <= x & x <= 122 ) by NAT_1:13;
then not not x = 114 & ... & not x = 122 ;
hence not x is prime by XPRIMES0:114, XPRIMES0:115, XPRIMES0:116, XPRIMES0:117, XPRIMES0:118, XPRIMES0:119, XPRIMES0:120, XPRIMES0:121, XPRIMES0:122; :: thesis: verum