:: deftheorem Def3 defines { ENUMSET1:def 3 :
for x1, x2, x3, x4, x5 being object
for b₆ being set holds
( b₆ = {x1,x2,x3,x4,x5} iff for x being object holds
( x in b₆ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) );