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