:: deftheorem Def8 defines { ENUMSET1:def 8 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being object
for b₁₁ being set holds
( b₁₁ = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for x being object holds
( x in b₁₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) );