:: deftheorem Def2 defines { ENUMSET1:def 2 :
for x1, x2, x3, x4 being object
for b₅ being set holds
( b₅ = {x1,x2,x3,x4} iff for x being object holds
( x in b₅ iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) );