let n be Nat; :: thesis: ( n satisfies_Sierpinski_problem_76a & n <= 181 implies n in {113,114,115,116,117,139,181} )
assume A1: n satisfies_Sierpinski_problem_76a ; :: thesis: ( not n <= 181 or n in {113,114,115,116,117,139,181} )
assume A2: n <= 181 ; :: thesis: n in {113,114,115,116,117,139,181}

per cases ( n <= 99 or n > 99 ) ;

suppose n <= 99 ; :: thesis: n in {113,114,115,116,117,139,181}

then not not n = 0 & ... & not n = 99 ;
hence n in {113,114,115,116,117,139,181} by A1, XPRIMES1:2, XPRIMES1:11, XPRIMES1:19, XPRIMES1:23, XPRIMES1:31, XPRIMES1:37, XPRIMES1:43, XPRIMES1:47, XPRIMES1:53, XPRIMES1:59, XPRIMES1:67, XPRIMES1:73, XPRIMES1:79, XPRIMES1:83, XPRIMES1:89, XPRIMES1:97, XPRIMES1:101; :: thesis: verum

end;

suppose n > 99 ; :: thesis: n in {113,114,115,116,117,139,181}

then ( n >= 99 + 1 & n <= 181 ) by A2, NAT_1:13;
then not not n = 100 & ... & not n = 181 ;
then ( n = 113 or n = 114 or n = 115 or n = 116 or n = 117 or n = 139 or n = 181 ) by A1, XPRIMES1:107, XPRIMES1:113, XPRIMES1:127, XPRIMES1:131, XPRIMES1:139, XPRIMES1:149, XPRIMES1:157, XPRIMES1:163, XPRIMES1:167, XPRIMES1:173, XPRIMES1:181;
hence n in {113,114,115,116,117,139,181} by ENUMSET1:def 5; :: thesis: verum

end;

end;