let n be Nat; :: thesis: ( n satisfies_Sierpinski_problem_87a & n <= 27 implies n in {13,17,21,23,27} )
assume A1: n satisfies_Sierpinski_problem_87a ; :: thesis: ( not n <= 27 or n in {13,17,21,23,27} )
assume n <= 27 ; :: thesis: n in {13,17,21,23,27}
then not not n = 0 & ... & not n = 27 ;
hence n in {13,17,21,23,27} by A1, Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11, Lm12, Lm13, Lm14, Lm15, Lm16, Lm17, Lm18, Lm19, Lm20, Lm21, Lm22, Lm23, Lm24, Lm25, Lm26, Lm27, ENUMSET1:def 3; :: thesis: verum