:: deftheorem Def1 defines { ENUMSET1:def 1 :
for x1, x2, x3 being object
for b₄ being set holds
( b₄ = {x1,x2,x3} iff for x being object holds
( x in b₄ iff ( x = x1 or x = x2 or x = x3 ) ) );