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