let n be Nat; :: thesis: ( n satisfies_Sierpinski_problem_86 & n <= 32 implies n in {14,16,20,22,32} )
assume A1: n satisfies_Sierpinski_problem_86 ; :: thesis: ( not n <= 32 or n in {14,16,20,22,32} )
assume n <= 32 ; :: thesis: n in {14,16,20,22,32}
then not not n = 0 & ... & not n = 32 ;
hence n in {14,16,20,22,32} by A1, Th50, Lm16, Lm17, Lm18, Lm19, Lm20, Lm21, Lm22, Lm23, Lm24, Lm25, Lm26, Lm27, Lm28, Lm29, Lm30, Lm31, Lm32, Lm33, Lm34, Lm35, Lm36, Lm37, ENUMSET1:def 3; :: thesis: verum