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